Semi-automatic verification of ISA security guarantees in the form of universal contracts

Description

Where ISA specifications used to be defined in
long prose documents, we have recently seen progress on
formal and executable ISA specifications. However, for now,
formal specifications provide only a functional specification
of the ISA, without specifying the ISA’s security guarantees.
In this paper, we present a novel, general approach to
specify an ISA’s security guarantee in a way that (1) can
be semi-automatically validated against the ISA semantics,
producing a mechanically verifiable proof, (2) supports in-
formal and formal reasoning about security-critical software
in the presence of adversarial code. Our approach is based
on the use of universal contracts: software contracts that
express bounds on the authority of arbitrary untrusted code
on the ISA. We semi-automatically verify these contracts
against existing ISA semantics implemented in Sail using our
Katamaran tool: a verified, semi-automatic separation logic
verifier for Sail. For now, in this paper, we will illustrate
our approach for MinimalCaps: a simplified custom-built
capability machine ISA. However, we believe our approach
has the potential to redefine the formalization of ISA security
guarantees and we will sketch our vision and plans.

Period	6 Sep 2021
Event title	SILM 2021 Workshop: Security of Software / Hardware Interfaces
Event type	Workshop