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


Informace, termíny:

Zde se objevují upozornění na nové závažné informace, blížící se termíny apod.
  • 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 30. 11. 2022 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. 2022 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.

Přednášky

Demonstrační příklady


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ů

  • 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 -- společnost neprodukuje přímo nástroj, ale nabízí 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)

  • 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
  • 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í

  • Coderrrect 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, biabdukce, 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)

  • SPEED -- symbolická analýza časových a prostorových nároků programů (tj. automatická analýza složitosti)
  • Loopus -- statická analýza zaměřená na automatickou analýzu složitosti u celočíselných programů v C

  • ...

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
  • Lingeling, Plingeling, Treengeling

  • 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

  • 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)
  • Retro -- nástroj pro ověřování splnitelnosti formulí nad řetězci (vyvíjený na FIT VUT)
  • Noodler -- nástroj pro ověřování splnitelnosti formulí nad řetězci (vyvíjený na 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)
  • Owl -- knihovna a toolbox pro práci s automaty nad nekonečnými slovy, LTL formulemi, hrami, syntézu a model checking
  • 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, ...

  • CSmith -- nástroj pro fuzz testování překladačů


Poslední modifikace: 13. December 2022
Připomínky k obsahu stránky posílejte na e-mail: vojnar@fit.vutbr.cz