Abstrakt. På senare tid har blockkedjeteknik, som lägger till poster till en lista med kryptografiska länkar, tillämpats i stor utsträckning inom det finansiella området. Därför är säkerheten i blockchain smarta kontrakt bland de mest populära samtida forskningsämnen. För att förbättra teorem-proving-tekniken inom detta område utvecklar vi en extensibel hybridverifieringsverktygskedja, betecknad som FSPVM-E, för Ethereum smart kontraktsverifiering. Detta hybridsystem utökar Coq-bevisassistenten, ett formellt bevishanteringssystem. Genom att kombinera symbolisk exekvering med högre ordningens teorem-proving löser den problem med konsekvens, automatisering och återanvändning genom standardiserade teorem-proving-metoder. Denna artikel kompletterar FSPVM-E genom att utveckla sin säkra motor. FSPVM-E är en extensibel definitionstolk baserad på vårt tidigare arbete Feather, som är helt utvecklad i Coq proof assistent. Den stöder nästan alla semantik av Solidity programmeringsspråk, och samtidigt utför flera typer av symboler. Fether innehåller också en uppsättning automatiska strategier som utför och verifierar de smarta kontrakten i Coq med en hög automationsnivå. Den funktionella korrektheten hos Fether verifierades i Coq. Effektiviteten i genomförandet av Fether överträffade vida den hos tolkarna som utvecklas i Coq i enlighet med standardhandledningen. Såvitt vi vet är Fether den första definitionstolken av Solidity-språket i Coq.
Yang och Lei REF utvecklade en definitionstolk Feather, som stöder hybrid symboliska utföranden av Ethereum smarta kontrakt formella kontroller i Coq.
FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq
{'venue': 'IEEE Access, 2019', 'journal': None, 'mag_field_of_study': ['Computer Science']}