A static verification framework for message passing in Go using behavioural types

January 25, 2018 ~ Adrian Colyer ~ 1 Comment

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

Linear Haskell: Practical linearity in a higher-order polymorphic language

January 24, 2018 ~ Adrian Colyer ~ 5 Comments

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

Why is random testing effective for partition tolerance bugs?

January 23, 2018 ~ Adrian Colyer ~ 1 Comment

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

Programming and proving with distributed protocols

January 22, 2018 ~ Adrian Colyer ~ Leave a comment

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

JaVerT: JavaScript Verification Toolchain

January 19, 2018 ~ Adrian Colyer ~ 4 Comments

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

RustBelt: securing the foundations of the Rust programming language

January 18, 2018 ~ Adrian Colyer ~ 2 Comments

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

Some thoughts on security after ten years of qmail 1.0

January 17, 2018 ~ Adrian Colyer ~ 21 Comments

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

Spectre attacks: exploiting speculative execution

January 16, 2018 ~ Adrian Colyer ~ 10 Comments

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

Meltdown

January 15, 2018 ~ Adrian Colyer ~ 12 Comments

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

One model to learn them all

January 12, 2018 ~ Adrian Colyer ~ 10 Comments

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

the morning paper

a random walk through Computer Science research, by Adrian Colyer
Made delightfully fast by strattic

Uncategorized