Toby's Blog

Yesterday, CrowdStrike released a post that contained a preliminary analysis of the technical causes of last week’s outage. That post finally sheds some light on how this incident occurred. More importantly, it lays out how CrowdStrike is planning to make sure this can’t happen again. CrowdStrike’s plan is totally inadequate in my assessment. In this post, I make sense of CrowdStrike’s explanation of what happened here and explain why their plan going forward is insufficient and what they should be doing instead. [Read More]

Updated: 2024-07-21 08:45 AM AEST: Clarifying that the Microsoft Azure outage in its Central US region began before the CrowdStrike update was pushed and so, despite claims in The Conversation from an Australian academic to the contrary, that outage was seemingly not caused by the CrowdStrike update. Updated: 2024-07-21 07:08 AM AEST: in the wake of blog posts from Microsoft, and CrowdStrike. In the last 24 hours there has been much written about the massive outage currently affecting Windows computers worldwide. [Read More]

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]