Bezpečnost, testování a formální verifikace

Jsme Runtime Verification, výzkumná a vývojová společnost budující rigorózní nástroje k zajištění bezpečnosti a správnosti kritických systémů. Náš tým vyvinul KEVM, nejkompletnější a praxí prověřenou formální sémantiku pro Ethereum Virtual Machine (EVM), napsanou v K Framework. KEVM není jen specifikace, je to spustitelná specifikace, kterou lze použít k symbolickému uvažování o chytrých kontraktech, spouštění testů shody, analýze spotřeby plynu (gas), ladění programů a formálnímu ověřování vlastností správnosti. Prochází celou testovací sadou Etherea a používá se k ověřování kontraktů s vysokou hodnotou, včetně tokenů ERC-20 v Solidity i Vyperu. Nedávno jsme aktualizovali sémantiku, aby podporovala aktualizaci Pectra. KEVM aktivně využívá Kontrol – náš nástroj pro formální verifikaci pro Solidity, který aktivně používají přední týmy v ekosystému EVM, včetně Optimism, Ethereum Foundation, Lido, Uniswap, a také bezpečnostní výzkumníci a auditoři napříč širší komunitou Etherea. Tento repozitář aktivně udržujeme, přispíváme k vývoji protokolu Etherea a integrujeme se s vývojářskými nástroji, jako je Foundry. Prostřednictvím KEVM posouváme hranice toho, co je možné v prokazatelně správné a bezpečné infrastruktuře chytrých kontraktů.

Generátor testů chytrých kontraktů založený na technice větvícího se stromu (Branching Tree Technique).

Společnost Runtime Verification je již více než deset let v popředí open-source nástrojů pro formální verifikaci. Náš obecný přístup nám umožňuje používat naši technologii na více blockchainech. Zatímco KEVM nabízí naši verifikační infrastrukturu všem chytrým kontraktům založeným na EVM, Kontrol výrazně snižuje bariéru vstupu do formální verifikace pro chytré kontrakty v Solidity. Naše nástroje jsou zcela open-source a volně přístupné všem vývojářům ekosystému Optimism bez dalších nákladů. KEVM je spustitelná formální sémantika EVM napsaná v K Framework. KEVM prochází všemi testy shody Etherea a je vstupním bodem pro formální ověřování chytrých kontraktů pomocí K Framework. Použití samotného KEVM však vyžaduje ad-hoc školení na K Framework pro psaní specifikací. Navíc tyto specifikace mohou být poměrně rozvláčné, což zvyšuje obtížnost jejich psaní. Kontrol to řeší tím, že umožňuje vývojářům psát formální specifikaci jejich chytrých kontraktů přímo jako testy vlastností ve Foundry. Tyto testy jsou automaticky překládány do specifikací KEVM, čímž jsou zachovány všechny záruky verifikace a zároveň je umožněna mnohem snazší vývojářská zkušenost.