Automatic Detecting Billion $ Coding Errors with Static Program Analysis

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

• Mooly Sagiv (Tel Aviv University)
• Friday 08 July 2022, 11:00-12:00
• Seminar Room 1, Newton Institute.

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.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.