Toby's Blog

Readers of my recent post, which tried to shed light on the use of LLMs to generate fuzzers, may have caught my undisguised skepticism towards the use of LLMs for static code analysis, especially for security vulnerability detection. In this post, I wanted to share a small CTF challenge that I wrote, which I designed to teach students to be similarly skeptical. (Or, if you prefer a more objective framing, let’s say I built the CTF challenge to teach students about the strengths and weaknesses of using LLMs for code analysis and understanding. [Read More]

LLMs seem surprisingly good at many things. So much so that not a week goes by without someone coming up with yet another use-case for this technology, often to solve tasks quickly that traditionally took a non-trivial amount of human work to complete. Today’s example was Brendan Dolan-Gavitt’s remarkable experiment using Claude to generate a fuzzer for some GIF parsing code. The entire thread is worth a read if you’re curious; however, Brendan gives Claude the C code for the GIF parser and asks Claude to generate the Python implementation for a fuzzer to generate GIF-like input to fuzz the given GIF parser. [Read More]

On Thursday Australia’s second-largest telecoms company, Optus, announced it had suffered a major data breach that had compromised sensitive customer information. Updated 2022-09-27 11:20 AM: To date, records of 10,200 individuals have been published online (the 10,000 records today and 200 records published earlier). While the purported attackers have since apparently promised that they have deleted their only copy of the data and will not release any further data online, there is no evidence yet to prove this claim (and indeed it is almost impossible to prove). [Read More]

If you’ve read my recent posts, you’ll know I’ve been thinking a fair bit about Wordle. You might also have picked up that I recently wrote and formally verified the core of a tiny Wordle implementation as being correct and secure, using the logic Security Concurrent Separation Logic (SecCSL) and its verifier, both largely developed by Gidon Ernst. Correctness means that when the player submits a guess, Wordle computes the right answer to return to them. [Read More]

Programmers love to set each other challenges, particularly ones that involve writing small programs whose jobs are seemingly simple but turn out to be quite difficult to write without making any mistakes. Such challenges have become a staple of job interviews at large and small tech companies alike. Here’s a parable about one such challenge. Brogrammer Bob is interviewing at a company who writes high-assurance software. His interviewer, Careful Carrie, asks him “Do you believe you can write perfect software? [Read More]

Semester starts next week. So what better time to write a blog post (the first in years). To hone my procrastination skills, I spent a couple hours playing around with Wordle this week, delving into its design and implementation. This is what I learned. The data on which this post is based was obtained by scripting some trivial (and sometimes horribly inefficient) analyses over the Wordle word lists. It’s all publicly available on github. [Read More]

tl;dr This post is about a recently published paper that takes a critical look at formal proofs as a means to assure the security of software systems, which I authored with Paul van Oorschot. I’m delighted to say that the paper received a Best Paper award at this year’s IEEE Cybersecurity Development Conference (SecDev). We argue that software proofs are poorly understood, especially outside formal methods researchers. Even amongst experts, however, there is disagreement about their precise value for producing secure software. [Read More]

Academia is sometimes portrayed as a noble pursuit. Yet I know that my own choice to become an academic was, at least partly, a selfish one. Researchers might talk about the greater good as their guiding motivation, but it’s worth remembering that many of us got into research simply because we loved doing research. Whether the joy of discovery and learning, getting to play at the forefront of knowledge, or just the ego trip of doing something unique: once you critically analyse there’s no shortage of selfish motivations. [Read More]

When I was a Computer Science undergraduate, at the turn of the millennium, by far the least engaging subjects that I studied were those on Software Engineering. Few know how to make Gantt charts exciting, and discussions of software development process models have never been my cup of tea, even if I did develop a real appreciation for empirical software engineering in the meantime. I deeply dig the irony, therefore, that I chose to be a Software Engineering teacher in 2016. [Read More]