References:
[1] ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. POPL, 2019
[2] CHERI ISA v8, 2020.
Architecture specifications define the fundamental interface between hardware and software: the envelope of allowd behaviour for processor implementations, and the basic assumtions for software development and verification.
Sail: an ISA semantic language with dependent type system.
A rigorous semantic models for the sequential behaviour of large parts of mainstream ARMv8-A, RISC-V, and MIPS archtitectures, and the research CHERI-MIPS architecture.
These architectures are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4.
ISA semantics defined in Sail.
Sail definition for validation;
Sail definition to assess specification coverage.
Functional correctness proof in Isabelle, for ARMv8-A address translation.
RMEM tool for (user-mode) relaxed-memory concurrency exploration, of RISC-V model.
Proof of the soundness of the core Sail type system.
A semantic for os-app interactions?
CHERI-MIPS From CHERI ISA v7. 2019. Conventions Specialregs Permissions is required to read special purpose capability registers, but CR3 is not included since it is not a capability register.
References: CHERI ISAv9 draft, 20221121 Sail is a domain specific imperative language designed for describing processor architectures. Sail in RISC-V instr. descriptions Constant Definitions Constants for 64-bit ISA with 128 bit capability: type xlen : Int = 64 type cap_addr_width : Int = xlen type cap_len_width : Int = cap_addr_width + 1 type cap_size : Int = 16 type cap_mantissa_width : Int = 14 type cap_hperms_width : Int = 12 type cap_uperms_width : Int = 4 type cap_uperms_shift : Int = 15 type cap_flags_width : Int = 1 type cap_otype_width : Int = 18 let cap_max_otype = MAX(cap_otype_width) - reserved_otypes Function Definitions Functions for integer and bit vector manipulation func 1:
MIPS pseudo instructions RISC-V Instructions Instructions dependent on encoding modes More Csc (ISAv7: Ch 7, p240) Format CSC cs, rt, offset(cb) CSCR cs, rt(cb) CSCI cs, offset(cb) Capability register cs is stored at memory location [cb.base + cb.offset + rt + 16 * offset], and the bit in the tag memory associated with this address is set to the value of cs.tag. Capability cb must contain a capability that grants permission to store capabilities.
Q&A Reference 1 ISA instructions MIPS encoding MIPS-IV encoding: MIPS-IV encoding.pdf R4000 Encoding.pdf I-Type (Immediate), 6 (op) + 5r + 5r + 16(i) J-Type (Jump), 6 (op) + 26 (index) R-Type (Register), 6 (op) + 5r + 5r + 5r + 5 (shift) + 6 (func) CHERI MIPS encoding ISAv7 Summary: all three-register-operand, non-memory-accessing CHERI-MIPS instructions using the following encodeing: | Bit | size | value | |—–|——|——-| | 31-26 | 6 | 0x12 | | 25-21 | 5 | 0x00 | | 20-16 | 5 | r1 | | 15-11 | 5 | r2 | | 10-6 | 5 | r3 | | 5-0 | 6 | func |
References: OS: https://github.com/Microsoft/cheriot-rtos Sail Model: https://github.com/Microsoft/cheriot-sail RTL: https://github.com/Microsoft/cheriot-ibex Blog: https://msrc-blog.microsoft.com/2022/09/06/whats-the-smallest-variety-of-cheri/ News 202302: https://www.microsoft.com/en-us/research/publication/cheriot-rethinking-security-for-low-cost-embedded-systems/ Whitepaper: https://www.microsoft.com/en-us/research/uploads/prod/2023/02/cheriot-63e11a4f1e629.pdf Overview Smallest CHERI (Portmeirion Project) RISC-V32. C extension required. 15 registers 32-bit address space A signle privilege level: Machine mode only. No virtual memory. Optional PMP. Optional floating point. Based on ibex. Ibex Implementation cite: https://github.com/Microsoft/cheriot-ibex RV32IMCB + CHERI. Either with 2-stage or 3-stage pipeline, configurable.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?