|
|
SAV: Informace pro studenty (zimní semestr 2024/2025)
Informace, termíny:
Zde se objevují upozornění na nové závažné informace, blížící se termíny
apod.
- Stream z přednášek je k dispozici na
YouTube.
- Vítám Vás všechny v kursu! Bude hodně o věcech, které jsou často
ještě předmětem intenzivního výzkumu, bude vyžadovat aktivitu z Vaší strany, ale
snad se Vám bude líbit a něco zajímavého se dozvíte.
- Projekt:
- Cílem projektu je bližší seznámení se s vybraným nástrojem pro statickou
analýzu a/nebo verifikaci a principy, na nichž je založen, reprodukce
dostupných případových studií pro zvolený nástroj (ideálně s nějakými
modifikacemi, aby se ověřilo, jak moc je nástroj vyladěn jen pro dané úlohy),
vlastní experimenty s uvedeným nástrojem, sepsání technické zprávy o zvoleném
nástroji a provedených experimentech. Výjimečně lze akceptovat i nástroj pro
dynamickou analýzu, který je založen na netriviálních formálních kořenech. Lze
také experimentovat s "podpůrnými" nástroji např. pro SAT/SMT solving, práci s
BDD apod.
- Projekt je za 30 bodů celkem. Výsledky projektů se odevzdávají
formou technické zprávy, která bude mít tři hlavní části:
- Popis nástroje, přičemž důraz je na
matematické/algoritmické/věcné principy, na kterých nástroj stojí.
Použití nástroje z uživatelského pohledu je možno uvést, ale v míře spíše
menší, ideálně jako odrazový můstek pro popis principů.
- Popis reprodukovaných experimentů: jaké experimenty byly
reprodukovány, s jakými výsledky, k jakým pokusům o modifikace došlo, jak
dopadly. (Pokud žádné stávající experimenty nejsou dostupné, je možno
je nahradit větším důrazem na níže uvedený bod.)
- Popis vlastních originálních experimentů: ideálně nad školními
projekty, volně dostupným software apod. (Uměle vytvořené příklady jsou
možné, ale ne úplně ideální, pokud neukazují něco zcela zásadního. Pouhá
modifikace parametrů či dílčích částí stávajících experimentů spadá do
výše uvedeného bodu.)
Každá část cca 3--5 stran v podobném formátu jako diplomová práce, každá za 10
bodů, hodnoceno dle míry zpracování a originality.
- Do 24. 11. 2024 je nutno registrovat nástroje, na které se
jednotliví studenti zaměří (jde zejména o kontrolu toho, zda se projekt
zaměřený na daný nástroj dá rozumně řešit -- pokud si vyberete triviální
nástroj, budete zřejmě mít problémy o něm něco sepsat). Registraci proveďte
zasláním emailu T. Vojnarovi.
- Termín odevzdání vypracované technické zprávy v pdf přes IS VUT/Moodle je
20. 12. 2023 12:00 CET.
- Průběžně doplňovaný seznam zaregistrovaných studentů pro řešení projektu
je uveden ZDE.
- Prémiové body (až 10 za vynikající výkon): Analýza zaměřená na
kód Linuxového jádra (či jiného otevřeného OS) či některého reálného open
source software, zejména v případě nalezení reálných nareportovaných
chyb.
- Odevzdání projektu: přes elearning (Moodle) VUT. Odevzdát je nutno
pdf soubor technické zprávy a volitelně zip/tgz s provedenými experimenty a
jejich výsledky.
Přednášky
Demonstrační příklady -- mimo již výše uvedené:
Monografie, přehledové články
- B. Křena, T. Vojnar. Automated Formal Analysis and Verification: An Overview. International Journal of General Systems, 42(4):335-365, Taylor and Francis, 2013.
- E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem (Eds.). Handbook of Model Checking. Springer, 2018.
- C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
- E.M. Clarke, O. Grumberg, D. Kroening, D. Peled., H. Veith. Model Checking, 2nd edition. MIT Press, 2018.
- G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.
- M. Ben-Ari. Principles of the Spin Model Checker. Springer, 2008.
- A. Valmari. The State Explosion Problem.
Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag 1998, pp. 429-528. (starší, ale stále zajímavé)
- X. Rival, K. Yi. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
- A. Moller, M.I. Schwartzbach. Static Program Analysis. Department of Computer Science, University of Aarhus, Denmark, 2021.
- F. Nielson, H.R. Nielson, C. Hankin. Principles of Program Analysis. Springer-Verlag, 2005.
- U. Khedker, A. Sanyal, B. Sathe. Data Flow Analysis: Theory and Practice. CRC Press, 2009. Na stránce jsou k dispozici také odpovídající slajdy.
- A.V. Aho, S. Lam, R. Sethi, J.D. Ullman.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. Část věnovaná statické analýze.
- B. Chess, J. West: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
- A.R. Bradley, Z. Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.
- D. Kroening, O. Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2016.
- A. Biere, M. Heule, H. Van Maaren, T. Walsh (Eds.). Handbook of Satisfiability. IOS Press, 2009.
- Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer, 2010.
- B.C. Pierce. Types and Programming Languages. The MIT Press, 2002.
- B.C. Pierce (Ed.). Advanced Topics in Types and Programming Languages. The MIT Press, 2004.
-
Nástroje -- experimentální i průmyslové
Upozornění: (1) Níže jsou uvedeny jen některé příklady existujících nástrojů, v žádném případě se nejedná o úplný seznam! (2) Uvedené krátké charakteristiky nebyly vždy získány na základě vlastní zkušenosti s příslušným nástrojem a nemusí být přesné -- naleznete-li nějakou nepřesnost či rozpor, prosím napište mi.
Competition on Software Verification (SV-COMP) -- mezinárodní soutěž ve verifikaci SW
- Model checking
- Spin -- verifikace (nejen) distribuovaných SW systémů, vstupem je specializovaný modelovací jazyk Promela (existují překladače do Promely z některých dalších jazyků)
- CPAchecker -- konfigurovatelný nástroj pro verifikaci software, zahrnuje model checking založený na predikátové abstrakci a interpolaci
- CBMC -- omezený model checking C programů
- ESBMC -- omezený model checking C programů
- Smack -- omezený model checking C
programů v kombinaci s řadou dalších analýz
- Blast
-- verifikace C programů (již starší nástroj), základem je predikátová abstrakce
a interpolace, nová verze je dostupná zde v rámci projektu Linux Driver Verification
- Divine -- model checking v
paralelním a distribuovaném prostředí s využitím řady vstupních formátů (včetně
C/C++)
- 2LS -- open source
analyzátor spojující principy omezeného model checkingu, k-indukce a abstraktní
interpretace vyvíjené i na FIT VUT
- DiffBlue -- firma stojící za
komercionalizací a dalším rozvojem např. CBMC či 2LS
- Ultimate
Automizer -- C model checker využívající predikátové abstrakce a teorie automatů
- Java PathFinder -- JPF --
verifikace a testování Java programů (viz i dále zmíněné nástroje s ním spojené)
- JBMC -- omezený model checking Java programů
- Lincheck -- omezený
model checking a stress testing paralelních Java/Scala/Kotlin programů
- Kani -- omezený
model checking Rust programů (AWS)
- JKind -- nekonečně stavový model checking synchronních systémů popsaných v jazyce Lustre
- NuSMV a NuXMV -- symbolický model checking (nejen) HW
- ABC -- systém pro syntézu a verifikaci HW (zahrnuje omezený model checking, včetně různých pokročilých technik vycházejících ze základních myšlenek BMC)
- Cadence Verification -- komerční nástroj pro verifikaci hardware od Cadence
- Questa Formal Verification Apps -- verifikace HW, Mentor Graphics
- Static
and Formal Verification at Synopsys -- verifikace HW, Synopsys
- Oski/NVIDIA
-- společnost neprodukovala přímo nástroj, ale nabízela verifikaci s využitím model
checkingu
- EBMC -- omezený model
checking pro Verilog (vychází ze CBMC)
- Uppaal -- model checking RT systémů popsaných časovanými automaty
- Prism -- pravděpodobnostní model checker nad Markovskými systémy
- Storm -- pravděpodobnostní
model checker nad Markovskými systémy, syntéza pravděpodobnostních systémů
(spolupráce i s FIT VUT)
- ProB -- model
checker podporující metodu B pro vývoj vestavěných kritických systémů (aplikace
např. v oblasti vlaků, metra apod.: Alstom, ClearSy, Siemens, Thales)
- TTool -- simulační i
formální verifikace spolehlivosti (safety), bezpečnosti (security) i výkonnosti
vestavěných systémů modelovaných pomocí SysML/UML s využitím model checkingu i
automatizovaného dokazování teorémů (security, kryptografie)
- nidhugg -- stateless
model checking pro paralelní programy se slabými paměťovými modely
- Concuerror -- stateless
model checking pro paralelní programy v jazyce Erlang
- TLA+ -- jazyk pro modelování systémů a protokolů a prostředí s model checkerem pro jejich verifikaci
- Apalache --
symbolický model checking TLA+ vysoko-úrovňových specifikací systémů
(Informal Systems)
- ...
- Statická analýza, analýza toku dat, abstraktní interpretace, symbolická exekuce, ...
- Přehled nástrojů pro statickou/dynamickou analýzu C kódu
- Seznam nástrojů pro statickou analýzu na Wikipedii
- Zajímavé srovnání některých nástrojů pro statickou analýzu
- Synopsys Static Analysis -- komerční nástroje pro
statickou analýzu C/C++/Java (chybové vzory, analýza toku dat, vylučování
nereálných chyb), dříve Coverity
- Klocwork -- komerční nástroje pro statickou analýzu C/C++/Java/C# (chybové vzory, analýza toku dat, vylučování nereálných chyb)
- CodeSonar -- komerční nástroje pro statickou analýzu C/C++ (chybové vzory, analýza toku dat, vylučování nereálných chyb)
- Microsoft Code analysis for C/C++ -- statická analýza vestavěná do VisualStudia, (zřejmě) chybové vzory a symbolická exekuce založená na využití SMT (Z3), možnost anotací
- Parfait -- interní nástroj v rámci Oracle, analýza toku dat, chybové vzory, ...
- Frama-C -- nástroj zahrnující abstraktní interpretaci pro C i deduktivní verifikaci C kódu anotovaného ACSL od francouzské agentury pro
atomovou energii (CEA)
- Facebook/Meta Infer -- komerční (ale open
source) nástroj založený na abstraktní interpretaci zaměřený na vybrané typy chyb
- Pluginy
pro Facebook Infer a Frama-C vyvíjené na FIT VUT
- MOPSA analyzer --
akademický framework pro tvorbu statických analyzátorů, hodně modulární,
postavený na abstraktní interpretaci a napsaný v OCamlu.
- Facebook SPARTA --
komerční (ale open source) prostředí pro tvorbu abstraktních interpretací
používané např. v optimalizátoru ReDex pro Android
- PhASAR -- prostředí pro tvorbu inter-procedurálních statických analýz nad C/C++ s důrazem na analýzu toku dat
- SeaHorn -- framework pro analýzu programů postavený nad LLVM využívající překladu programů do Hornových klauzulí a jejich následné řešení
- Coderrect Scanner -- statická analýza
(ukazatelová analýza, analýza toku dat) specializovaná pro detekci chyb typu
"data race"
- Slam a Static Driver Verifier -- verifikace driverů v MS Windows, dříve s využitím predikátové
abstrakce, nyní s využitím symbolické exekuce založené na SMT
- KLEE -- kombinace statické analýzy založené na symbolickém provádění a testování
- Symbiotic -- kombinuje instrumentaci kódu o monitory sledující verifikované vlastnosti, slicing a symbolickou exekuci (existuje i kombinace s nástrojem Predator
- SymbolicPathFinder
(SPF) -- rozšíření výše uvedeného nástroje JPF pro symbolickou exekuci Java programů
- Java Ranger --
úprava výše uvedeného nástroje SPF s podporou slučování symbolických cest
- JDart -- úprava výše uvedeného nástroje JPF pro konkolické provádění
- Gillian -- separační logika,
symbolické provádění pro JavaScript a C
- Certora Prover -- symbolická
exekuce pro formální verifikaci smart kontraktů (Certora). K dispozici také
další nástroje: fuzz testing.
- FindBugs -- volně dostupný nástroj pro statickou analýzu Javy (chybové vzory, analýza toku dat)
- SpotBugs -- nástupce FindBugs
- Clang Static Analyzer -- statický analyzátor pro C a Objective C, využívá chybové vzory, analýzu toku dat
- Statická
analýza v GCC -- statická analýza založená na chybových vzorech (např.
double-free, use-after-free) v rámci gcc
- SonarQube -- analýza toku dat a
chybové vzory pro vybrané chyby v kódu i zranitelnosti z hlediska bezpečnosti
nad řadou různých jazyků
- Cppcheck -- statický analyzátor pro C/C++, relativně jednoduché vyhledávání chybových vzorů v toku řízení
- cppclean -- statická analýza programu v C++, vyhledávání chybových vzorů nad AST
- Sparse -- statická analýza pro jádro Linuxu
- Cobra
-- interaktivní lightweight statická analýza zaměřená na vyhledávání chybových
vzorů ve velmi velkých programech (od G. Holzmanna, autora Spinu, použito mj. v
NASA)
- OpenScanHub -- lightweight statická
analýza i dynamická analýza, obaluje řadu nástrojů jako cppcheck a zpřístupňuje
je přátelsky vývojářům (použito mj. při vývoji RHEL)
- DiffKemp -- využití
statické analýzy pro ověřování, zda při refaktoringu nedochází k nežádoucím
změnám sémantiky, aplikováno např. na jádro RHEL či GNU Linux (spolupráce Red
Hat a FIT VUT)
- AbsInt a Astrée -- komerční nástroje pro statickou analýzu (abstraktní interpretaci) vestavěných systémů, zejména analýzu časování, práce se zásobníkem a ověřování absence runtime chyb (spolehlivá)
- PolySpace -- komerční nástroje pro statickou analýzu vestavěných systémů reálného času v
C, C++, Adě (abstraktní interpretace)
- Daisy -- analýza toku dat a analýza založená na optimalizačních problémech pro analýzu a optimalizaci numerických programů
- TAJS -- statická analýza pro
JavaScript
- gdfa: A Generic
Data Flow Analyzer for GCC -- jednoduché generické prostředí pro tvorbu
analýz toku dat (demonstrující principy z knihy Uday P. Khedker, Amitabha
Sanyal, Bageshri Karkare: Data Flow Analysis: Theory and Practice)
- Predator -- nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými
datovými strukturami z FIT VUT (využívá grafy, v principu založen na separační logice)
- Forester
-- starší, již nevyvíjený nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými datovými strukturami z FIT VUT (založen na stromových automatech)
- AProVE -- kombinace abstraktní interpretace pro ověření korektnosti práce s pamětí a vystavění abstraktního modelu, následovaná různými technikami pro dokazování konečnosti/složitosti běhu (s využitím SMT)
- Loopus -- statická analýza
zaměřená na automatickou analýzu složitosti u celočíselných programů v C (viz i
jeho reinkarnace v rámci prostředí Infer (pluginy pro Infer z FIT VUT)
- ...
- Theorem proving, SAT solving, SMT solving, rozhodovací procedury
- PVS -- interaktivní theorem prover
- Coq -- interaktivní theorem prover
- HOL -- interaktivní theorem prover
- ACL2 -- interaktivní theorem prover
- Lean -- interaktivní theorem prover
- Vampire -- plně automatický theorem prover pro predikátovou logiku s řadou dalších zajímavých funkcionalit (výpočet interpolantů apod.)
- SAT Competition -- soutěž o nejlepší nástroj pro řešení SAT problému
- MapleSAT
- Kissat SAT Solver
- CaDiCaL
- SMT-Comp -- soutěž o nejlepší nástroj pro řešení problémů SMT (SAT modulo teorie)
- Z3
- MathSAT
- CVC5
- Yices2
- Boolector
- SMTInterpol
- what4 -- knihovna pro tvorbu analyzátorů nad SMT
- Z3str3RE a
Z3str4 -- nástroje pro ověřování
splnitelnosti formulí nad řetězci postavené nad SMT solverem Z3
- Noodler -- nástroj pro ověřování splnitelnosti formulí nad řetězci (vyvíjený na FIT VUT)
- Retro -- nástroj pro ověřování splnitelnosti formulí nad řetězci (vyvíjený na FIT VUT)
- Z3-Trau -- nástroj pro ověřování splnitelnosti formulí nad řetězci (spolupráce s FIT VUT)
- Sloth -- nástroj pro ověřování splnitelnosti formulí nad řetězci (spolupráce s FIT VUT)
- Ostrich -- nástroj pro ověřování splnitelnosti formulí nad řetězci
- MONA -- nástroj pro ověřování platnosti formulí logik WS1S a WS2S (jde o slabé monadické logiky druhého řádu, používáné často pro usuzování např. o stromových datových strukturách)
- SL-COMP -- soutěž o nejlepší
nástroj pro splnitelnost/inkluze formulí separační logiky (vhodná pro popis
konfigurací programů s ukazateli a dynamickými datovými strukturami)
- Astral -- nástroj pro rozhodování
silně-separační logiky (vyvíjený na FIT VUT)
- Facebook/Meta Infer
Biabduction -- nástroj založený na separační logice a tzv. bi-abdukci pro
programy s ukazateli a seznamy
- Broom
-- první prototyp nástroje založený na separační logice a bi-abdukci pro
programy s ukazateli, seznamy a nízko-úrovňovou manipulací s pamětí (vyvíjený na FIT VUT)
- VCC -- verifikace anotovaných programů v C
- Nagini -- verifikace anotovaných programů v Pythonu
- ESC/Java2 -- verifikace anotovaných programů v Javě
- ...
- Automaty nad nekonečnými slovy
- Spot -- knihovna a toolbox pro práci s automaty nad nekonečnými slovy, LTL formulemi, hrami, syntézu a model checking (včetně Jupyter bindingu pro interaktivní práci)
- Ranker -- nástroj pro rank-based komplementaci Büchiho automatů (vyvíjený na FIT VUT)
- Kofola -- nástroj pro decomposition-based komplementaci Büchiho automatů (vyvíjený na FIT VUT)
- GOAL -- Java knihovna a GUI pro interaktivní práci s automaty nad nekonečnými slovy
- BDD
- CUDD -- knihovna pro práci s BDD a jejich variantami
- BuDDy -- knihovna pro práci s BDD
- Sylvan -- knihovna pro práci s BDD a jejich variantami zaměřená na vícevláknové zpracování
- Analýza a verifikace neuronových sítí
- alpha-beta-CROWN --
založeno na aproximujících optimalizačních metodách s využitím efektivních
výpočetních heuristik
- Eran -- analýza robustnosti
neuronových sítí s využitím abstraktní interpretace
- DeepGame -- verifikace
neuronových sítí s využitím teorie her
- Reluplex -- verifikace
neuronových sítí s využitím SMT
- Dynamická analýza, pokročilé testování
- ANaConDA -- nástroj pro dynamickou analýzu paralelních C/C++ programů na binární úrovni vyvíjený na FIT VUT
- Perun --
nástroj pro dynamickou analýzu výkonnosti programů (využívající i statickou
analýzu z jiných nástrojů), automatická detekce výkonnostních regresí,
optimalizovaný profiling -- vyvíjený na FIT VUT
- RoadRunner --
nástroj pro dynamickou analýzu paralelních Java programů
- psharp-ql --
testování paralelních programů řízené učením
- Valgrind -- dynamická analýza (založená
na interpretaci) korektní práce s pamětí, vlákny, ...
- Coyote -- systematické
testování (se snahou vybírat zajímavá proložení) paralelního kódu od firmy
Microsoft, použito např. v rámci vývoje Microsoft Azure...
Poslední modifikace:
Připomínky k obsahu stránky posílejte na e-mail:
vojnar@fit.vutbr.cz
|