Ethereum är ett ramverk för cryptocurrencies som använder blockchain-teknik för att tillhandahålla en öppen global datorplattform, kallad Ethereum Virtual Machine (EVM). EMM kör bytekod på en enkel stack maskin. Programmerare skriver vanligtvis inte EVM-kod; istället kan de programmera på ett JavaScript-liknande språk, kallat Solidity, som kompilerar till bytecode. Eftersom det huvudsakliga syftet med EMM är att utföra smarta kontrakt som hanterar och överför digitala tillgångar (så kallade Ether ), är säkerhet av största vikt. Skriva säkra smarta kontrakt kan dock vara mycket svårt: på grund av öppenheten i Ethereum, både program och pseudonym användare kan kalla in offentliga metoder för andra program, vilket leder till potentiellt farliga sammansättningar av betrodda och opålitlig kod. Denna risk illustrerades nyligen av en attack på TheDAO kontrakt som utnyttjade subtila detaljer av EMM semantics för att överföra ungefär $ 50M värde av Ether till kontroll av en angripare. I detta dokument beskriver vi ett ramverk för att analysera och verifiera både säkerheten i drifttiden och den funktionella korrektheten av Ethereum kontrakt genom översättning till F, ett funktionellt programmeringsspråk som syftar till programverifiering.
Bhargavan m.fl. REF skisserade ett ramverk för att analysera och verifiera både körtidens säkerhet och den funktionella korrektheten hos Ethereumkontrakt genom översättning till F*, ett funktionellt programmeringsspråk som syftar till programverifiering.
Formal Verification of Smart Contracts: Short Paper
{'venue': "PLAS '16", 'journal': None, 'mag_field_of_study': ['Computer Science']}