University of Cambridge > > Isaac Newton Institute Seminar Series > Automatic Detecting Billion $ Coding Errors with Static Program Analysis

Automatic Detecting Billion $ Coding Errors with Static Program Analysis

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

Static program analysis is a well-understood technique for identifying programming errors. However, static analysis techniques are not used in practice due to the high rate of false alarms (i.e., reported errors that are not real) and because most errors reported typically indicate low-level internal programming errors (which are usually not security-critical) such as violations of memory safety.  We describe a precise static technique for detecting violations of high-level properties of low-level bytecode programs. We apply the technique to detect violations in smart contracts that manipulate billions of dollars through transactions on the blockchain.  The user specifies a high-level specification expected from the program. The system automatically detects transitions from valid to invalid states. For example, one such violation allows a transaction to completely drain all money in a contract. Fortunately, these violations are detected before the code is deployed. Our system first converts the low-level bytecode and the specification into a simple three-address IR and then harnesses SMT solvers for identifying faults in the resulting programs. Since memory is represented as a low-level array of bytes at the bytecode level, the system implements a sound points-to analysis that enables the SMT solvers to use a more structured representation of memory rather than the naive low-level representation.

This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity