Collapsing Towers of Interpreters

Research Goal

Modern computer stacks run over multiple levels of abstraction. A payroll form might use formulas written into a spreadsheet, which is executed by the spreadsheet’s internal evaluator, which is implemented in Javascript, running in a browser, and so on. Because each layer has its own distinct semantics, reasoning at the level of the complete system is difficult, with errors often creeping in at the boundaries. Even worse, layers may not even have consistent semantics – a Python interpreter may dynamically load performance instrumentation for certain functions mid-flight.

There is a way out. Via staged programming and specialization, we propose to collapse this tower into one program, operating under one semantics, which can be analyzed with classic tools.

Our goals are twofold:

Current Projects

Collapsing Towers for Side-Channel Security

Much recent attention has been placed on microarchitectural side-channel attacks, where hardware-level optimizations are exploited to leak information about a supposedly-secure process through differences in execution time. We propose to address this by collapsing the abstract semantics of the top-level program with the underlying hardware semantics to reify such side channel information into a form more amenable to formal verification. Then, we can use off-the-shelf static analyzers to discover and repair microarchitectural flaws.

Papers

Collaborators