bitauth / bitauth-ide

an online IDE for bitcoin (cash) contracts
https://ide.bitauth.com
MIT License
78 stars 15 forks source link

Linting, security analysis via symbolic execution #12

Open bitjson opened 5 years ago

bitjson commented 5 years ago

It's probably not too difficult to programmatically determine if e.g. the locking script isn't secure against miners. Simplest check is to see if a checksig operation was done for each path.

If you'd be interested in this feature, please comment here.

bitjson commented 3 years ago

Linting idea: recommend any evaluation with only one push be simplified to remove the unnecessary syntax: from $(< X >) to X.

bitjson commented 2 years ago

Linting + autofix idea: find all script segments which include stack juggling operations: OP_DUP OP_2DUP OP_3DUP OP_NIP OP_TUCK OP_DROP OP_2DROP OP_SWAP OP_2SWAP OP_OVER OP_2OVER OP_ROT OP_2ROT OP_TOALTSTACK OP_FROMALTSTACK <2> OP_PICK <3> OP_PICK <4> OP_PICK <5> OP_PICK <3> OP_ROLL <4> OP_ROLL <5> OP_ROLL, run the segment on a stack of 1 2 3 4 5 6 to get the resulting transformation, then pass the expected input/output to a stack operation optimizer. If the segment can be optimized, suggest/autofix to the more efficient construction.

bitjson commented 2 years ago

RE: validation, we can definitely build a symbolic execution engine that demonstrates if a locking script has unhandled unlocking conditions (some set of inputs which unlock the script which aren't represented by a known unlocking script in the template) to verify the security of a particular contract.