A static verification framework for message passing in Go using behavioural types Lange et al., ICSE 18 With thanks to Alexis Richardson who first forwarded this paper to me. We’re jumping ahead to ICSE 18 now, and a paper that has been accepted for publication there later this year. It fits with the theme we’ve … Continue reading A static verification framework for message passing in Go using behavioural types
Category: Uncategorized
Linear Haskell: Practical linearity in a higher-order polymorphic language
Linear Haskell: Practical linearity in a higher-order polymorphic language Bernardy et al., POPL 18 I went in expecting this paper to be hard work. I mean, (a) it’s a POPL paper, (b) it’s about Haskell, and (c) not only is it about Haskell, it’s about an extension to the Haskell type system! I was more … Continue reading Linear Haskell: Practical linearity in a higher-order polymorphic language
Why is random testing effective for partition tolerance bugs?
Why is random testing effective for partition tolerance bugs? Majumdar & Niksic, POPL 18 A little randomness is a powerful thing! It can make the impossible possible (FLP ), balance systems remarkably well (the power of two random choices), and of course underpin much of cryptography. Today’s paper choice examines the unreasonable effectiveness of random … Continue reading Why is random testing effective for partition tolerance bugs?
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
Meltdown
Meltdown Lipp et al., 2018 I’m writing this approximately one week ahead of when you get to read it, so it’s entirely possible by this time that you’ve already heard more than you can stand about Meltdown and Spectre! Behind the news headlines though, there’s a lot of good information in the accompanying papers, and … Continue reading Meltdown
One model to learn them all
One model to learn them all Kaiser et al., arXiv 2017 You almost certainly have an abstract conception of a banana in your head. Suppose you ask me if I’d like anything to eat. I can say the word ‘banana’ (such that you hear it spoken), send you a text message whereby you see (and … Continue reading One model to learn them all
the morning paper 