M221 Advanced Compilers and Static Analysis

Course info

Spring semester, Thu 2-5pm, classroom B

Instructor: Yannis Smaragdakis

Piazza signup link

Background:

The course will cover topics in static program analysis. We will be using logic-based specifications, in the Datalog language, to express static analyses over an intermediate language. Our platform of experimentation will be an IR for Ethereum smart contracts. This is a critical modern domain that greatly benefits from static analysis.

The course is a seminar and requires active participation. The last hour of every meeting will be hands-on coding and support on the currently active assignment. You will need to bring a laptop (or pair productively with someone who brings one).

Policies:

• 4 homework assignments (at 60%), final exam (40%)
• Paper presentations (1-2) throughout semester

Homeworks

Submission by email, by midnight of the deadline.

• HW1
• HW2
• HW3
• HW4

Slides, notes

• IRs, data-flow analysis
• Ethereum background
• Interpreter specification
• Andersen-style value-flow analysis
• Andersen-style analysis in Datalog (context-sensitive)
  • Points-to tutorial survey
• Mathematical logic and Datalog practice
• Soundness/Soundiness discussion

Papers

• Securify
• Symbolic execution survey
• Steensgaard points-to analysis
• Soundiness
• Static analysis of JavaScript dynamic features

Tools, resources

• Souffle Datalog implementation
• Gigahorse-toolchain
• Gigahorse-benchmarks
• contract-library