Not so fast: Analyzing the performance of {WebAssembly} vs. native code
All major web browsers now support WebAssembly, a low-level bytecode intended to serve
as a compilation target for code written in languages like C and C++. A key goal of …
as a compilation target for code written in languages like C and C++. A key goal of …
ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS
A Armstrong, T Bauereiss, B Campbell, A Reid… - Proceedings of the …, 2019 - dl.acm.org
Architecture specifications notionally define the fundamental interface between hardware
and software: the envelope of allowed behaviour for processor implementations, and the …
and software: the envelope of allowed behaviour for processor implementations, and the …
QED at large: A survey of engineering of formally verified software
Abstract Development of formal proofs of correctness of programs can increase actual and
perceived reliability and facilitate better understanding of program specifications and their …
perceived reliability and facilitate better understanding of program specifications and their …
A complete formal semantics of x86-64 user-level instruction set architecture
We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our
semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of …
semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of …
Using safety properties to generate vulnerability patches
Security vulnerabilities are among the most critical software defects in existence. When
identified, programmers aim to produce patches that prevent the vulnerability as quickly as …
identified, programmers aim to produce patches that prevent the vulnerability as quickly as …
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats
It is a neat result from functional programming that libraries of parser combinators can
support rapid construction of decoders for quite a range of formats. With a little more work …
support rapid construction of decoders for quite a range of formats. With a little more work …
The high-level benefits of low-level sandboxing
Sandboxing is a common technique that allows low-level, untrusted components to safely
interact with trusted code. However, previous work has only investigated the low-level …
interact with trusted code. However, previous work has only investigated the low-level …
An abstract stack based approach to verified compositional compilation to machine code
A key ingredient contributing to the success of CompCert, the state-of-the-art verified
compiler for C, is its block-based memory model, which is used uniformly for all of its …
compiler for C, is its block-based memory model, which is used uniformly for all of its …
A verified protocol buffer compiler
Q Ye, B Delaware - Proceedings of the 8th ACM SIGPLAN International …, 2019 - dl.acm.org
The code responsible for serializing and deserializing untrusted external data is a vital
component of any software that communicates with the outside world, as any bugs in these …
component of any software that communicates with the outside world, as any bugs in these …
[PDF][PDF] Compiling sandboxes: Formally verified software fault isolation
Software Fault Isolation (SFI) is a security-enhancing program transformation for
instrumenting an untrusted binary module so that it runs inside a dedicated isolated address …
instrumenting an untrusted binary module so that it runs inside a dedicated isolated address …