Progress has recently been made on specifying instruction set architectures (ISAs) in executable formalisms rather than through prose. However, to date, those formal specifications are limited to the functional aspects of the ISA and do not cover its security guarantees. We present a novel, general method for formally specifying an ISAs security guarantees to (1) balance the needs of ISA implementations (hardware) and clients (software), (2) can be semi-automatically verified to hold for the ISA operational semantics, producing a high-assurance mechanically-verifiable proof, and (3) support informal and formal reasoning about security-critical software in the presence of adversarial code. Our method leverages universal contracts: software contracts that express bounds on the authority of arbitrary untrusted code. Universal contracts can be kept agnostic of software abstractions, and strike the right balance between requiring sufficient detail for reasoning about software and preserving implementation freedom of ISA designers and CPU implementers. We semi-automatically verify universal contracts against Sail implementations of ISA semantics using our Katamaran tool; a semi-automatic separation logic verifier for Sail which produces machine-checked proofs for successfully verified contracts. We demonstrate the generality of our method by applying it to two ISAs that offer very different security primitives: (1) MinimalCaps: a custom-built capability machine ISA and (2) a (somewhat simplified) version of RISC-V with PMP. We verify a femtokernel using the security guarantee we have formalized for RISC-V with PMP.

翻译：近期，在指令集架构（ISA）的可执行形式化规范方面取得了进展，而非依赖自然语言描述。然而，迄今为止，这些形式化规范仅限于ISA的功能层面，并未涵盖其安全保证。我们提出了一种新颖的通用方法，用于形式化规范ISA的安全保证，以（1）平衡ISA实现（硬件）与客户端（软件）的需求，（2）可半自动验证其对ISA操作语义的保持性，生成高可信度的机械可验证证明，以及（3）支持在存在对抗性代码的情况下对安全关键软件进行非形式化与形式化推理。我们的方法利用通用契约：这类软件契约表达了对任意不可信代码权限的约束。通用契约可独立于软件抽象层面，并在为软件推理提供足够细节与保留ISA设计者及CPU实现者实现自由度之间达成恰当平衡。我们使用Katamaran工具（一款针对Sail语言、支持半自动分离逻辑验证并生成机器检查证明的工具）对ISA语义的Sail实现进行半自动验证。通过将方法应用于两种提供截然不同安全原语的ISA，我们展示了其通用性：（1）MinimalCaps：一款定制的能力机器ISA；（2）RISC-V的（略简化版）PMP方案。我们利用为RISC-V PMP形式化的安全保证，验证了一个女仆级内核。