Oyente-based Bounded Model Checker (OBMC)

[leonardoalt]

Hi, I've been working on a bounded model checker (I've been calling it OBMC) based on Oyente (it's in my fork, branch master). The approach is different from Oyente's, in the sense that OBMC (as a standard SMT-based bounded model checker) creates a single SMT formula that encodes the values symbolically (like Oyente does) plus all the program paths and conditions as well, instead of simulating all the paths and calling z3 separately for each path (loops are unrolled up to the given limit). The graph traversal to build the SMT formula is linear, and the exponential path traversal is left to the solver (instead of an explicit exponential traversal). This single formula built by OBMC is of course much more complex than the single path formulas given to z3 by Oyente, but OBMC is running faster than Oyente when checking assertions (slower on some cases that I know they lead to even more complex formulas, I can elaborate on that later). So far the SMT encoding only looks for assertion fails, but it should be possible to encode more behaviors and let the solver do the heavy work.

So my question to you guys is: are you interested in working on and/or discussing the BMC approach? The code looks quite different from Oyente right now, as the approach is different, so I think a pull request wouldn't make much sense. As I mentioned, I've been calling it OBMC (Oyente BMC), but I can change it if you don't feel that's appropriate.

[loiluu]

Hi @leonardoalt I think OBMC is a great idea and it is definitely a different approach than Oyente. However, i doubt the practicality of it since its not always feasible to generate a giant formula to simulate all program paths. Are you able to get some statistics to compare the performance between OBMC and Oyente?

In terms of the PR, i suggest merging to the same code base here since 1) we can concentrate the developing and testing efforts; 2) users can enjoy different approaches from one single tool. I do realise the major difference in the codebase though.

[leonardoalt]

Hi @loiluu The formula isn't that big, since its size is linear on the size of the CFG. In fact, for more complicated cases, the time to build the graph (for now it does explore exponentially the CFG to find all jump targets without doing any computation, only PUSHs and POPs) is longer than the SMT solving time. I have a few examples which I'm using for development and debugging, not really a benchmark suite. After I get to a stable version I'll compare times better using the examples in ethereum/solidity.

We could have it in a separate branch then, such that we don't mix the code.

[joeykrug]

https://github.com/AugurProject/augur-core would be a good benchmark suite, there's not many more complex dapps than it

[1ultimat3]

@leonardoalt: I am really interested in your work. Would it be possible to verify liveness properties - e.g. in the sense of CTL/LTL?

[1ultimat3]

Easy example, consider Ethernaut's King Level https://ethernaut.zeppelin.solutions/level/0x32d25a51c4690960f1d18fadfa98111f71de5fa7):

..
 function() external payable {
    require(msg.value >= prize);
    king.transfer(msg.value);
    king = msg.sender;
    prize = msg.value;
  }

Actually what I would like to verify is that the function is always terminated or some condition is true after the function call (even if the revert is triggered):

function() external payable {
  ... //previous code
    // in the attack revert() is called 

   assert(we finished this method, check values);
  //alternative liveness check
   assert(no deadlock here)
  }

[leonardoalt]

@mateuszk87 If the sentence you want to prove can be represented in Solidity, it can also be checked (in a bounded way). There are exceptions such as external calls etc. If you want to verify liveness in general I guess you would need some CTL/LTL extensions. You could also just restrict the liveness checks and make custom queries that represent those.

[yxliang01]

Hey @leonardoalt ! I am really interested in OBMC , I think it sounds really cool. I am wondering, have you finished implementing it?

Thanks