Rocksalt: better, faster, stronger SFI for the x86. Software-based fault isolation (SFI), as used in Google’s Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google’s original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level verification tasks
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos: System-level non-interference of constant-time cryptography. I: Model (2019)
- Tan, Gang; Morrisett, Greg: Bidirectional grammars for machine-code decoding and encoding (2018)
- Blazy, Sandrine; Laporte, Vincent; Pichardie, David: Verified abstract interpretation techniques for disassembling low-level self-modifying code (2016)