The Three-Body Problem trilogy, by brilliant Chinese author Cixin Liu, is a triumph of human creativity that I’ve previously extolled as one of the greatest sci-fi epics of all time. This short story was written in 2016, and is based off of events in the spectacular final book, Death’s End.
Category: pwnable | Points: 124 | Solves: 49 | Challenge files
This is a classic C++ menu challenge that features a UAF and heap overflow with a vtable pointer overwrite. The main heap techniques involve using a free unsorted bin chunk to leak a libc and heap address, as well as some feng shui to place an object in an overflow-able region on the heap. fortenforge, qzqxq, and I combined to reverse the binary and discover the 3 separate vulnerabilities.
I discovered my interest in film at the start of college. As an arts reviewer for The Tech, MIT’s student newspaper, I had the luxury of attending advance press screenings of big-name films like Suicide Squad and the final Hobbit film. But more importantly, my reviews cultivated an appreciation for the medium and an insatiable desire to experience all it had to offer. Since then, I’ve devoured films of all genres and eras, directors and actors, cinematographers and writers.
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.
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.
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.
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.
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.
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.