Programming and proving with distributed protocols

Programming and proving with distributed protocols Sergey et al., POPL 18 Last week we looked at the verification of Rust’s type-based safety guarantees, and a verification toolchain for proving properties of JavaScript programs. Today it’s the turn of Disel, a framework for developing and verifying message-passing based distributed systems (it would seem to fit beautifully … Continue reading Programming and proving with distributed protocols

JaVerT: JavaScript Verification Toolchain

JaVerT: JavaScript Verification Toolchain Santos et al., POPL 18 The JavaScript Verification Toolchain (JaVerT) is designed to support reasoning over JavaScript programs. It can be used to verify functional correctness properties of programs annotated with pre- and post- conditions, loop invariants, and instructions for unfolding and folding user-defined predicates. To do this, it must be … Continue reading JaVerT: JavaScript Verification Toolchain

RustBelt: securing the foundations of the Rust programming language

RustBelt: Securing the foundations of the Rust programming language Jung et al., POPL, 2018 Yesterday we saw the value of meta-engineering development processes in order to produce better (more secure) outcomes. Included in Bernstein’s recommendations was careful selection of programming language. Rust is a language in that spirit. It has long been a “holy grail” … Continue reading RustBelt: securing the foundations of the Rust programming language

Some thoughts on security after ten years of qmail 1.0

Some thoughts on security after ten years of qmail 1.0 Bernstein, 2007 I find security much more important than speed. We need invulnerable software systems, and we need them today, even if they are ten times slower than our current systems. Tomorrow we can start working on making them faster. That was written by Daniel … Continue reading Some thoughts on security after ten years of qmail 1.0

Spectre attacks: exploiting speculative execution

Spectre attacks: exploiting speculative execution Kocher et al., 2018 Yesterday we looked at Meltdown and some of the background on how modern CPUs speculatively execute instructions. Today it’s the turn of Spectre of course, which shares some of the same foundations but is a different attack, not mitigated by KAISER. On a technical front, Spectre … Continue reading Spectre attacks: exploiting speculative execution