ELVER-CHECK: Well-grounded Lightweight Assurance for Critical Systems Software

Introduction

Computer systems have become critical to modern society, but they are pervasively subject to security flaws and attacks. This includes large-scale exposures of confidential data, denial-of-service and ransom attacks, and the threat of nation-state attackers: they are trusted, but are far from trustworthy.

Importance of Systems Software

This is especially important for the systems software that enforces what protection is in place, e.g., the hypervisors that use the underlying hardware to isolate components from each other.

Development of Mathematical Models

ERC AdG ELVER has developed mathematical models of the systems features of the underlying hardware. This involves working with Arm to characterize:

1. Virtual memory
2. Instruction/data cache maintenance
3. Exceptions

This opens up a new possibility: using these models not just for correctness proof (which remains challenging), but also for lightweight methods to improve the assurance of critical systems software.

Targets and Applications

The focus is on checking that such software obeys the subtle disciplines required by the hardware. Targets include:

• The pKVM hypervisor being developed by Google to protect sensitive data on all Android phones
• Similar hypervisors for the Cloud

Building on experience with a prototype checker, which has already found subtle bugs, ELVER-CHECK will prototype, assess, and demonstrate how to use executable checkers based on our mathematical models of systems architecture. This aims to improve the conventional development of critical systems software, increasing assurance that it provides the intended security at a lower cost than full verification.

Societal Impact

ELVER-CHECK thus addresses an important aspect of the societal problem of the pervasive insecurity of our critical software infrastructure.

New Opportunities in Software Testing

This is a new opportunity: conventional software testing, analysis, and verification methods assume that memory is a simple mapping from locations to values. However, they are oblivious to the subtle ways in which this is simply not true for systems software, and to the disciplines that it must follow to actually enforce the intended security properties.