Dafny, FDR4 i Isabelle sprawdzają różne klasy własności
Dafny, FDR4 i Isabelle nie są trzema wariantami tego samego weryfikatora. Każde narzędzie przyjmuje inny artefakt wejściowy i rozstrzyga inny rodzaj pytania: zgodność implementacji z kontraktem, zgodność procesu współbieżnego ze specyfikacją albo poprawność twierdzenia zapisanego w logice formalnej.
Dafny sprawdza implementację względem kontraktów zapisanych w kodzie
Dafny jest językiem programowania z konstrukcjami specyfikacji. Kontrakty metod opisuje się przez warunki wejściowe i wyjściowe, a pętle przez niezmienniki. Można również określić zbiory odczytywanych i modyfikowanych danych oraz miary terminacji.
Weryfikator tłumaczy program na warunki dowodowe, przekazuje je przez Boogie do solvera SMT, zwykle Z3, i sprawdza, czy kontrakt wynika z implementacji. Po udanej weryfikacji kod Dafny może zostać skompilowany między innymi do Javy.
Dafny nadaje się do sprawdzania własności odnoszących się do stanu programu: poprawności wyniku, zachowania niezmienników, dostępu do pamięci i zakończenia obliczenia. Nie potwierdza, że kontrakt opisuje właściwe wymaganie biznesowe. Nie sprawdzi też protokołu komunikacji wielu usług, jeśli ten protokół nie zostanie jawnie zamodelowany.
FDR4 porównuje zachowanie procesów zapisanych w CSP
FDR4 analizuje modele zapisane w CSPM, maszynowej wersji algebry procesów CSP. Model opisuje zdarzenia, możliwe kolejności komunikatów, wybory, synchronizację oraz zachowanie równolegle działających procesów.
Narzędzie sprawdza relację refinementu pomiędzy specyfikacją a implementacją modelową. W zależności od wybranego modelu semantycznego może wykryć:
- ślad zdarzeń, którego specyfikacja nie dopuszcza;
- stan, w którym proces odmawia zdarzenia wymaganego przez specyfikację;
- deadlock;
- nieskończoną sekwencję kroków wewnętrznych, czyli livelock.
Po naruszeniu własności FDR4 zwraca kontrprzykład w postaci śladu prowadzącego do błędnego stanu. Dzięki temu nadaje się do analizy protokołów, maszyn stanów i koordynacji procesów. Nie weryfikuje bezpośrednio kodu Java. Najpierw trzeba zbudować model CSP i określić jego związek z implementacją.
Isabelle sprawdza twierdzenia zapisane w wybranej logice
Isabelle jest ogólnym asystentem dowodzenia. Najczęściej używana konfiguracja, Isabelle/HOL, udostępnia logikę wyższego rzędu, definicje typów danych, funkcji rekurencyjnych i relacji indukcyjnych. Twierdzenia oraz kolejne kroki dowodu zapisuje się w języku Isar, a system sprawdza ich poprawność.
Isabelle może opisać własności, które nie pasują bezpośrednio do kontraktu metody ani do refinementu procesu CSP. Można w niej dowodzić równoważności modeli, własności transformacji, poprawności semantyki języka albo tego, że spełnienie zestawu założeń implikuje wymaganą własność bezpieczeństwa.
Większa ekspresyjność oznacza więcej pracy przy formalizacji definicji, lematów i powiązań pomiędzy poziomami modelu. Isabelle nie generuje dowodu poprawności całego systemu na podstawie samego repozytorium.
Dobór narzędzia zależy od sprawdzanej własności
| Narzędzie | Artefakt wejściowy | Typowe pytanie | Wynik błędu |
|---|---|---|---|
| Dafny | program i kontrakty | Czy implementacja spełnia warunki wejściowe, wyjściowe i niezmienniki? | niespełniony warunek dowodowy i lokalizacja w programie |
| FDR4 | procesy CSPM | Czy model implementacji jest refinementem specyfikacji i nie zawiera deadlocku lub livelocku? | ślad zdarzeń prowadzący do naruszenia |
| Isabelle | definicje i twierdzenia w logice formalnej | Czy wskazane twierdzenie wynika z przyjętych definicji i założeń? | niedomknięty cel dowodowy |
W potoku generującym kod z użyciem LLM Dafny może sprawdzać kontrakty implementacji, FDR4 protokół współbieżności, a Isabelle relację pomiędzy modelem domenowym i własnością bezpieczeństwa. Użycie wszystkich trzech narzędzi ma sens tylko wtedy, gdy system rzeczywiście zawiera te trzy rodzaje zobowiązań dowodowych.
Transformacje pomiędzy modelami są częścią zaufanej bazy
Jeżeli kod Java jest automatycznie tłumaczony na modele dla Dafny, CSP lub Isabelle, dowód dotyczy wygenerowanego modelu. Błąd translatora może spowodować, że narzędzie poprawnie zweryfikuje artefakt, który nie odpowiada zachowaniu kodu źródłowego.
Architektura takiego potoku powinna więc jawnie wersjonować translatory, testować je na znanych przypadkach pozytywnych i negatywnych oraz przechowywać powiązanie pomiędzy fragmentem kodu, modelem i zobowiązaniem dowodowym. Bez tego status „verified” informuje o modelu po transformacji, ale nie daje wystarczającego dowodu o implementacji uruchamianej w produkcji.
42az⁝ Zielony build nie wystarcza. Jak projektować weryfikację dla kodu pisanego przez agentów AI
Wykorzystuję treści generowane przez AI jako część mojego codziennego procesu nauki.