1

I was reading this article

https://diligence.consensys.net/files/D1T2%20-%20Bernhard%20Mueller%20-%20Smashing%20Ethereum%20Smart%20Contracts%20for%20Fun%20and%20ACTUAL%20Profit.pdf

and came across a line on page 10

Using LASER, we can represent smart contract execution as a space of states and path formulas in propositional logic. Obviously, this   in itself is a mind-blowing achievement, but how is it useful for security analysis?

I would like to know what is this correlation between LASER and Smart Contracts or in general with Ethereum?

Also if anyone can point me in the direction of how this is useful and further reading would be helpful

Possible clues I had are it has something to do with Mythril

1

In page 4 at the last line they define it as:

LASER-Ethereum is a symbolic interpreter for Ethereum bytecode. Given one or more smart contract accounts as input, it returns a set of abstract program states. A state consists of the set of values that the virtual machine variables (such as the program counter, virtual machine stack, and account balances) take at a particular point during execution.

And in the github website: https://github.com/b-mueller/laser-ethereum. They say it is a:

LASER is a symbolic virtual machine (SVM) that runs Ethereum smart contracts. It accurately models most features of the Ethereum virtual machine including inter-contracts calls.

it helps you know with this if it run into the problem, it can give you the certain input and the trace for you reproduce it. So you don’t need to waste a lot of time to try every random input

To understand about symbolic execution you can follow these link:

https://en.wikipedia.org/wiki/Symbolic_execution

https://cs.stackexchange.com/questions/92742/how-symbolic-execution-works

https://youtu.be/yRVZPvHYHzw

disclaimer: i haven’t used this but according to what i read and research about it for 1 hour this is what i can do. If you see anything that is wrong please tell me.

| improve this answer | |
  • Thank you so much for every input given by you. TBH, I am also quite new to this kind of thing and was digging in the direction of smart contract security and came across this. After reading your links and answer, I now have an general idea about this thing and also came to knew that it is related to CS field and my question was just a subset kind of thing. I would definitely let you know if anything new pops up in my research – Hackeerrrr Feb 19 at 5:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.