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）基于PMP的（经过适当简化的）RISC-V版本。我们利用为基于PMP的RISC-V所形式化的安全保证，验证了一个femtokernel。