Формална верификација

У контексту хардверских и софтверских система, формална верификација представља чин доказивања или оспоравања исправности система у односу на одређену формалну спецификацију или својство, коришћењем формалних математичких метода.[1] Формална верификација је кључни подстицај за формалну спецификацију система и налази се у језгру формалних метода. Она представља важну димензију анализе и верификације у аутоматизацији електронског дизајна и један је од приступа верификацији софтвера. Употреба формалне верификације омогућава највиши ниво процене (EAL7) у оквиру заједничких критеријума за сертификацију рачунарске безбедности.

Формална верификација може бити корисна у доказивању исправности система као што су: криптографски протоколи, комбинациона кола, дигитална кола са унутрашњом меморијом и софтвер изражен као изворни код у програмском језику. Значајни примери верификованих софтверских система укључују верификовани C компајлер CompCert и језгро оперативног система са високим нивоом поузданости seL4.

Верификација ових система се спроводи обезбеђивањем постојања формалног доказа математичког модела система.[2] Примери математичких објеката који се користе за моделирање система укључују: коначни аутомат, означене прелазне системе, Хорнове клаузуле, Петријеве мреже, системе сабирања вектора, временске аутомате, хибридне аутомате, процесну алгебру, формалну семантику програмских језика као што су операциона семантика, денотациона семантика, аксиоматска семантика и Хорова логика.[3]

Приступи

Један од приступа и формација је провера модела, која се састоји од систематски исцрпне експлорације математичког модела (ово је могуће за коначне моделе, али и за неке бесконачне моделе где се бесконачни скупови стања могу ефективно представити коначно коришћењем апстракције или искоришћавањем симетрије). Обично се то састоји у истраживању свих стања и прелаза у моделу, коришћењем паметних и домен-специфичних техника апстракције како би се разматрале целе групе стања у једној операцији и смањило време рачунања. Технике имплементације укључују нумерацију просторa стања, симболичку нумерацију простора стања, апстрактну интерпретацију, симболичку симулацију, и рафинацију апстракције. Својства која треба верификовати често се описују у темпоралним логикама, као што су линеарна темпорална логика (LTL), језик за спецификацију својстава (PSL), SystemVerilog Assertions (SVA),[4] или компјутерска логика стабала (CTL). Велика предност провере модела је што је често потпуно аутоматска; њен главни недостатак је што се углавном не скалира добро на велике системе; симболички модели су обично ограничени на неколико стотина битова стања, док експлицитна нумерација стања захтева да простор стања који се истражује буде релативно мали.

Други приступ је дедуктивна верификација. Она се састоји од генерисања скупа математичких доказних обавеза из система и његових спецификација (и могућих других анотација), чија истинитост имплицира усклађеност система са његовом спецификацијом, и решавања тих обавеза коришћењем асистената за доказивање (интерактивних теорема доказивача), као што су HOL, ACL2, Isabelle, Coq или PVS, или аутоматских доказивача теорема, укључујући посебно решаваче задовољивости модуло теорија (SMT). Недостатак овог приступа је што може захтевати од корисника да детаљно разуме зашто систем ради исправно и да ту информацију пренесе систему за верификацију, било у облику низа теорема које треба доказати, или у облику спецификација (инваријанти, предуслови, постуслови) компоненти система (нпр. функција или процедура), а можда и поткомпоненти (као што су петље или структуре података).

Софтвер

Формална верификација софтверских програма подразумева доказивање да програм задовољава формалну спецификацију свог понашања. Подобласти формалне верификације укључују дедуктивну верификацију (види горе), апстрактну интерпретацију, аутоматизовано доказивање теорема, типске системе и лаке формалне методе. Један обећавајући приступ верификацији заснован на типовима је програмирање са зависним типовима, у коме типови функција укључују (барем делимично) спецификације тих функција, а проверавање типова кода утврђује његову исправност у односу на те спецификације. Језици са потпуним подршком за зависно типизирање омогућавају дедуктивну верификацију као посебан случај.

Још један допунски приступ је извођење програма, где се ефикасан код производи из функционалних спецификација кроз серију корака који очувавају исправност. Пример овог приступа је Бирд-Мертенсова формализација, и овај приступ се може сматрати другом формом исправности кроз конструкцију.

Ове технике могу бити звучне, што значи да се верификована својства могу логички извести из семантике, или незвучне, што значи да нема такве гаранције. Звучна техника даје резултат тек када је обухватила цео простор могућности. Пример незвучне технике је она која покрива само подскуп могућности, на пример само целе бројеве до одређеног броја, и даје „довољно добар“ резултат. Технике такође могу бити одлучиве, што значи да су њихове алгоритамске имплементације гарантују да ће се завршити са одговором, или неодлучиве, што значи да можда никада неће завршити. Ограничавањем обима могућности могуће је конструисати незвучне технике које су одлучиве када звучне технике које су одлучиве нису доступне.

Верификација и валидација

Верификација је један аспект тестирања подобности производа за његову сврху. Валидација је комплементарни аспект. Често се цео процес провере назива V & V (верификација и валидација).

  • Валидација: "Да ли покушавамо да направимо праву ствар?", односно, да ли је производ спецификован у складу са стварним потребама корисника?
  • Верификација: "Да ли смо направили оно што смо покушавали да направимо?", тј. да ли производ одговара спецификацијама?

Процес верификације се састоји од статичких/структурних и динамичких/понашајних аспеката. На пример, за софтверски производ може се прегледати изворни код (статички) и извршити тестирање против специфичних тест случајева (динамички). Валидација се обично може извршити само динамички, тј. производ се тестира стављањем у типичне и атипичне сценарије употребе ("Да ли задовољава све случајеве употребе?").

Аутоматизована поправка програма

Поправка програма се изводи у складу са "ораклом", што представља жељену функционалност програма која се користи за валидацију генерисаних исправки. Један једноставан пример је тест-скуп — парови улаз/излаз дефинишу функционалност програма. Разне технике се користе, најзначајније укључујући решаваче задовољивости модуло теорија (SMT) и генетичко програмирање,[5] које користи еволуциону рачунарску методу за генерисање и оцену могућих кандидата за исправке. Први метод је детерминистички, док је други случајан.

Поправка програма комбинује технике формалне верификације и синтезе програма. Технике локализације грешака у формалној верификацији користе се за одређивање тачака у програму које могу бити могућа места грешака, која могу бити мета модула за синтезу. Системи за поправку често се фокусирају на малу предефинисану класу грешака како би смањили простор претраге. Индустријска употреба је ограничена због рачунарских трошкова постојећих техника.

Коришћење у индустрији

Раст комплексности дизајна повећава значај формалних верификационих техника у индустрији хардвера.[6][7] Тренутно, формална верификација се користи од стране већине или свих водећих компанија у области хардвера,[8] али њена примена у индустрији софтвера и даље је ограничена. Ово се може приписати већој потреби у индустрији хардвера, где грешке имају веће комерцијалне последице. Због потенцијалних суптилних интеракција између компоненти, све је теже обухватити реалан скуп могућности симулацијом. Важни аспекти дизајна хардвера су погодни за аутоматизоване методе доказивања, што чини формалну верификацију лакшом за увођење и продуктивнијом.[9]

До 2011. године, неколико оперативних система је формално верификовано: NICTA-ов Secure Embedded L4 микројезгро, продаван комерцијално као seL4 од стране OK Labs; [10]OSEK/VDX базирани реално-временски оперативни систем ORIENTAIS са East China Normal University универзитета; оперативни систем Integrity компаније Green Hills Software; и PikeOS компаније SYSGO.[11] [12]У 2016. години, тим који је предводио Zhong Shao на Универзитету Јејл развио је формално верификовано оперативно језгро под називом CertiKOS.[13][14]

До 2017. године, формална верификација је примењена на дизајн великих рачунарских мрежа путем математичког модела мреже [15] и као део нове категорије технологија мрежа, мрежа заснованих на намерама. [16] Провајдери софтвера за мреже који нуде решења за формалну верификацију укључују Cisco, [17] Forward Networks[18][19] и Veriflow Systems. [20]

Програмски језик SPARK пружа алате који омогућавају развој софтвера уз формалну верификацију и користи се у неколико система високог интегритета.

Компилатор CompCert C је формално верификовани C компилатор који имплементира већину ISO C стандарда. [21][22]

Види такође

  • Аутоматизовано доказивање теорема
  • Провера модела
  • Списак алата за проверу модела
  • Формална провера једнакости
  • Провера доказа
  • Језик спецификације својстава
  • Статичка анализа кода
  • Темпорална логика у верификацији коначних стања
  • Пост-силиконска валидација
  • Интелигентна верификација
  • Верификација у време извршења

Референце

  1. ^ Sanghavi, Alok (21. 5. 2010). „What is formal verification?”. EE Times Asia. 
  2. ^ Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick, ур. (2018). Handbook of Model Checking (на језику: енглески). Cham: Springer International Publishing. ISBN 978-3-319-10574-1. 
  3. ^ „Introduction to Formal Verification”. ptolemy.berkeley.edu. Приступљено 2024-09-12. 
  4. ^ Winikoff, M. (2010), Assurance of Agent Systems: What Role Should Formal Verification Play?, Springer US, стр. 353—383, ISBN 978-1-4419-6983-5, Приступљено 2024-09-12 
  5. ^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley. „GenProg: A Generic Method for Automatic Software Repair”. IEEE Transactions on Software Engineering. 38 (1): 54—72. ISSN 0098-5589. 
  6. ^ Harrison, J. (2003). „Formal verification at Intel”. IEEE Comput. Soc: 45—54. ISBN 978-0-7695-1884-8. doi:10.1109/LICS.2003.1210044. 
  7. ^ Umrigar, Z.D.; Pitchumani, V. (1983). „Formal Verification of a Real-Time Hardware Design”. 20th Design Automation Conference Proceedings. IEEE. 19: 221—227. doi:10.1109/dac.1983.1585652. 
  8. ^ Seligman, Erik; Schubert, Tom; Kumar, M V Achutha Kiran (2015), Formal verification, Elsevier, стр. 1—22, ISBN 978-0-12-800727-3, Приступљено 2024-09-12 
  9. ^ Hunt, James J. (2012), The Practical Application of Formal Methods: Where Is the Benefit for Industry?, Springer Berlin Heidelberg, стр. 22—32, ISBN 978-3-642-31761-3, Приступљено 2024-09-12 
  10. ^ „Original PDF”. dx.doi.org. Приступљено 2024-09-12. 
  11. ^ Baumann, Christoph; Beckert, Bernhard; Blasum, Holger; Bormer, Thorsten (2012-11-26). „Lessons Learned From Microkernel Verification — Specification is the New Bottleneck”. Electronic Proceedings in Theoretical Computer Science. 102: 18—32. ISSN 2075-2180. doi:10.4204/eptcs.102.4. 
  12. ^ Ganssle, Jack G. (2000), Real Time Means Right Now!, Elsevier, стр. 53—85, ISBN 978-0-7506-9869-6, Приступљено 2024-09-12 
  13. ^ Harris, Robin (David Ronald), (born 22 June 1952), writer, Oxford University Press, 2007-12-01, Приступљено 2024-09-12 
  14. ^ Gold, Steve. „German firm develops world's first “Trojan-proof” password system”. Infosecurity. 5 (7): 8. ISSN 1754-4548. doi:10.1016/s1754-4548(08)70112-8. 
  15. ^ Beshley, Mykola; Klymash, Mykhailo; Beshley, Halyna; Urikova, Oksana; Bobalo, Yuriy (2021-12-10), Future Intent-Based Networking for QoE-Driven Business Models, Springer International Publishing, стр. 1—18, ISBN 978-3-030-92433-1, Приступљено 2024-09-12 
  16. ^ Tsuzaki, Yoshiharu; Okabe, Yasuo (2017). „Reactive configuration updating for Intent-Based Networking”. 2017 International Conference on Information Networking (ICOIN). IEEE. 15: 97—102. doi:10.1109/icoin.2017.7899484. 
  17. ^ Ao, Weng Chon; Psounis, Konstantinos. „Data-Locality-Aware User Grouping in Cloud Radio Access Networks”. IEEE Transactions on Wireless Communications. 17 (11): 7295—7308. ISSN 1536-1276. doi:10.1109/twc.2018.2866055. 
  18. ^ RAND Review: January-February 2018. RAND Corporation. 2018. 
  19. ^ Getting in: Data collection in grounded theory, SAGE Publications Ltd, 2018, стр. 31—48, Приступљено 2024-09-12 
  20. ^ CROWN-PRINCE RETRIEVED: LIFE AT CUSTRIN NOVEMBER 1730-FEBRUARY 1732, Cambridge University Press, 2010-11-11, стр. 342—406, Приступљено 2024-09-12 
  21. ^ Separation logic for CompCert, Cambridge University Press, 2014-04-21, стр. 141—141, Приступљено 2024-09-12 
  22. ^ Barrière, Aurèle; Blazy, Sandrine; Pichardie, David (2023-01-09). „Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler”. Proceedings of the ACM on Programming Languages (на језику: енглески). 7 (POPL): 249—277. ISSN 2475-1421. doi:10.1145/3571202.