Thanks to Vlad Brown and Drawings Team for Russian and Uzbek translations.

In Fall 2017, I took MIT’s 6.826, Principles of Computer Systems, taught by Turing Award-winner Butler Lampson, Nickolai Zeldovich, and Frans Kaashoek. Despite its rudimentary title, it’s a grad class on building formally verified systems. Using the proof language Coq, we wrote specifications, implementations, and proofs of toy structures: a remapped disk, an atomic pair of blocks, and a replicated disk. We also read quite a few papers from the state-of-the-art in formal methods.

I went into the class believing that formal verification is the future — the only solution to a world of software ridden with bugs and security issues. But after recent events and a semester of trying to apply formal methods, I’m a serious skeptic. In this post, I’ll discuss why I think formal verification has a long way to go — and why it just doesn’t work right now.

Read More

In this post, I’ll walk through how to link an application against LLVM and show a simple usage of the LLVM McDisassembler API. It’s a little more complex that it seems, probably because there’s not many good resources for using this API.

Read More

I’m currently taking the Fall 2017 iteration of 6.826, Principles of Computer Systems. This class has been offered in various forms over the years, but this iteration is quite different. It focuses on formal verification of computer systems using Coq, a language for mechanical theorem proving.

The goal of this class is to write the spec, implementation, and proofs for a formally verified RAID filesystem in Coq, then generate Haskell code from it.

Read More

Into uncharted waters we venture… this set has some various problems about famous real-world vulnerabilities, and it was challenging. fortenforge and I worked together quite a bit to get through it.

Read More

I’ve been wanting to write this post for a while — here I’ll describe all the excellent customizations that I’ve accrued over several years of optimizing my Mac for speed and alleviating repetitive stress injury (RSI). If you’re a Mac power user, or if you make a living at a keyboard, you want to read this.

Read More

It’s always bothered me that MIT or MIT Lincoln Lab didn’t submit anything to DARPA’s Cyber Grand Challenge. With all the smart people, such as my advisor, Armando Solar-Lezama, working on program analysis and formal methods (which I currently know nothing about), I would have expected that we could create a strong Cyber Reasoning System worthy of CGC.

That’s sort of what I will be working on this summer at Lincoln and probably writing my thesis on. But I’m very new to the field and have just started diving in.

Read More

The last of the original crypto challenges… here we go!

Challenge 41 Implement unpadded message recovery oracle

Unpadded RSA is homomorphic, meaning that, if operations like multiplication and addition are carried out on ciphertext, it is as if the same operation were applied to the plaintext.

Read More

Update 5/5/17: We qualified to DEF CON CTF 2017!!! We just got the email today! Congrats to everyone from Lab RATs, TechSec, and RPISEC that competed. Vegas, here we come!

Read More

Well, this was my first foray into the world of Rust, the systems language that is Mozilla’s precious baby. And what better way to learn this hip new language than to write an MITScript bytecode interpreter for Computer Language Engineering?

Rust was not gentle for this first-time developer. It does so much to protect you that my first attempt writing a few hundred lines of code resulted in the same number of compiler errors, and I needed a lot of help from my team to just get anything to compile. For this reason, it’s not great for iterating quickly if you aren’t very experienced already. But, I’m licking my chops at the fact that the end result will be much safer, and hopefully faster, than our classmates’ C++ compilers. This post will be about the struggles I encountered as a Rust newbie, as well as the fun of generating/interpreting MITScript bytecode.

Read More

This set was surprisingly easy, actually. The book Understanding Cryptography by Paar & Pelzl is an excellent intro to the basic maths needed for crypto — namely, the group theory and number theory necessary for RSA and Diffie-Hellman.

Let’s dive in!

Challenge 33 Implement Diffie-Hellman

Diffie-Hellman is a remarkably simple algorithm for two parties to jointly compute a shared secret key that may be used, for example, as a key for symmetric encryption.

Alice and Bob agree on an integer group of prime $p$, with a generator $g$. $g$ raised to every power in ${0...p-1}$, taken $\bmod p$, can produce every element of $p$. Hence, it is called a “generator” of the group.

Read More