Formal Verification on Smart Contract slides: https://hackmd.io/p/rJzvzC9TN#/
Hello, everyone, I am chen yixi from cheng kung university. So, what is formal verification? and why do we need formal verification?
Debug challenges.
We had already spend a lot of time debuging compared to developing, and sometimes can not even make sure the efforts on debugging is actually meaningful.
Most of the time, we have to deal with something we are not familiar with. So we have to use profiler or debuger to trace or sometime guess the workflow.
Confusing operations
For example, this is a very simple C implentation of getting an absolute value from a integer. If you are not used to bitwise operation, this might be a little confusing. And, if you think more about this function, how do we prove the correctness of this implementation ?
The first idea come into my mind might solve it with brute force, under current processor structure, we assume the whole operation took 50 cycles, so for a 32-bit integer, we will have to use 30 seconds for verification.
And for 64-bit integer, we will then have to use almost 4000 years only to verify this simple function.
Why not just edge case ?
It sounds ridiculous to you, at least to me. So we use test case to detect some frequent mistakes like integer overflow. But how can we ganurantee the coverage of such test case ? And this is the exact counterexample for this implementation.
Compute arbitrary-precision square roots.
That is just a simplied example, and this is an real implementation on getting sqare root. This is way harder to get the meaningful test case.
And you might think, "it was all because the bad alignment of the coding style"
#define crBegin static int state=0; switch(state) { case 0:
#define crReturn(x) do { state=__LINE__; return x; \
case __LINE__:; } while (0)
#define crFinish }
int decompressor (void ) {
static int c, len;
crBegin;
while (1 ) {
c = getchar()
if (c == EOF) break ;
if (c == 0xFF ) {
len = getchar();
c = getchar();
while (len--) crReturn(c);
} else crReturn(c)
}
crReturn(EOF);
crFinish; }
Co-routined version of a decompressor for RLE
Designing testcase to verify the correctness is always available, however, it is hard to evaluate the effectness and coverage of different test case. Especially when we didn't have a concrete expectation on the specification.
I assumed that everybody has already know what is blockchain and smart contract, while Blockchain is a distributed ledger, and smart contract helps automate the trading process.
Cryptocurrency Theft
We all heard about huge finanical loss on cryptocurrency, the security issue is somehow different than what we used to see before.
Take the DAO event for example, this is a simplified version of the buggy function.
Normal Usecase
Atomic operation ?
This is how the function "withdraw" should used. When someone, that say, the Wallet Contract tries to withdraw money from Contract DAO, it call function withdraw in Contract DAO, then function withdraw evaluate the value, then call back to Wallet Contract to notify it to receive money, and then modify DAO's balance.
Re-entrancy Abuse
However, if we change the "receiver function" in Wallet Contract to call withdraw again, since DAO hasn't modify its balance yet, the attacker will be able to call withdraw function for unlimited time in this section.
Smart Contract Challenges
Transactions are processed after a delay Adversaries can re-order and “frontrun” transactions All smart contract data is public Execution is expensive (gas costs, tx fees) Code is difficult to change (“Code is law”)
Bitcoin can take hours to confirm a tranction The order of transaction within a time section is not ganuaranteed.
Verification Tools
So there are many automatic verification tool to assure the correctness of smart contract. Today we'll be focus on KEVM.
Formal Verfication
In KEVM, we re-write the spec into a formal semantic, and then verify it with the proof checker, in KEVM, it is pretty similar to compiler frontend, plus state transition to detect if there is a illegal operation.
Formal Semantics
EIP 20: ERC-20 Token Standard
So, what is formal semantics? Let's look at the ERC20-spec, erc20 spec is a smart contract standard for exchanging ethereum to other 3rd party token. As you can see here, there are some interface like balanceof(), approve(), and today we will be focus on transferfrom()
Transfrom() allow the 3rd party account to help transfer money from other account to account, the caller should be the 3rd party account, and from account, to account.
Before the 3rd party account calls "transferFrom()", from_account should first call approve() function to permit 3rd party account for a certain amount of money. This make sense, right?
Allowance: Should we modify it ? Gas: Potential Gas Depletion ?
But what if the to_account and from_account is the same account ? First, should we modify the allowance since it is a weird transaction ? And since it should always be successful, do we have to check the transfer value to make sure it is small enough ? Finally, the meaningless contraction also consume gas, which might in the end deplete the total gas storage ?
Formal Verfication Is Not A Magic runtimeverification/erc20-semantics/erc20.k
/*uint128 a = 1*/
Formal Semantic is the requirement of conducting formal verification, formal verfication is not a magic, you must have to be fully aware of the whole structure behavior and possible side effects, otherwise, it is totally useless. Especially while nowadays project structures are getting more and more complex, the difficulty to construct a formal semantic is getting harder and harder. So formal verification requires lots of time and efforts, so it is too hard for massive deployment.
Formal Verification
But if you make it to the correct formal semantic of your specs and implementations, then we can move on to formal verification. Formal verification use the concept of symbolic execution. Take these two implementation for example, according to ERC20-spec, the totalSupply function should return the 3rd party token total amount, and the upper one should be the correct one, while the lower one is the crappy one.
Symbolic execution
When there is a branch situatation, the workflow will split into applying different corresponding rule, and the whole graph is construct with series of condition state. Once the graph is completed, it will verify each available execution path by choosing a representing number that fullfill all the condition along with its path, and compare the result with spec and implementation.
when supply != 0x1000 … 0000
when supply == 0x1000 … 0000
Resume presentation
Formal Verification on Smart Contract slides: https://hackmd.io/p/rJzvzC9TN#/ Hello, everyone, I am chen yixi from cheng kung university. So, what is formal verification? and why do we need formal verification?
{"metaMigratedAt":"2023-06-14T21:59:04.375Z","metaMigratedFrom":"YAML","title":"Formal Verification on Smart Contract","breaks":true,"description":"View the slides with \"Slide Mode\".","contributors":"[{\"id\":\"55530dc6-d89b-405e-b1f3-65fc1e8faa0d\",\"add\":17986,\"del\":8325},{\"id\":\"98f90f3d-f96e-47cf-bd6b-8f9476eb04d5\",\"add\":2,\"del\":2}]"}
