SAV: Informace pro studenty (zimní semestr 2023/2024)


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.
  • 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:
      1. 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ů.
      2. 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.)
      3. 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 28. 11. 2023 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 23. 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


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ů

  • 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

  • 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

  • ...

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

  • 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
  • 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)
  • 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: 5. January 2024
Připomínky k obsahu stránky posílejte na e-mail: vojnar@fit.vutbr.cz