W zeszłym tygodniu na OOPSALA '25 nasi deweloperzy Act zaprezentowali ulepszoną, skalowalną wersję CheckMate, automatycznego dowodnika do formalnej weryfikacji bezpieczeństwa teoretycznego gier protokołów blockchain. Krótko mówiąc: narzędzie sprawdza, czy zachęty w protokole sprawiają, że oszustwo nie jest opłacalne.

Protokoły potrzebują 3 rodzajów bezpieczeństwa: • Kryptograficzne: Czy twoje klucze/hasła są silne? • Implementacyjne: Czy w kodzie są błędy? • Teoretyczno-gier: Czy zachęty są dostosowane tak, aby oszustwo się nie opłacało? Ten ostatni jest kluczowy, ale często ignorowany.

Bezpieczeństwo oparte na teorii gier polega na zapewnieniu, że nawet racjonalni, egoistyczni aktorzy wolą przestrzegać zasad - ponieważ odstąpienie od nich kosztuje więcej, niż przynosi zysku. To jest "ekonomia" bezpieczeństwa.

CheckMate formalnie i automatycznie dowodzi bezpieczeństwa teoretycznego gier przy użyciu rozwiązywaczy SMT. Artykuł wprowadza kompozycyjną algorytm "dziel i rządź", który skaluje się do milionów węzłów, przeplatając generację modeli i analizę dla zwiększenia efektywności.

Dlaczego to ma znaczenie: Teraz możemy automatycznie, formalnie i na dużą skalę udowodnić, że zachęty protokołu blockchain sprawiają, że oszustwo jest nieracjonalne - przed wdrożeniem.