Recent content on Toby's Blog
On 21 July, OpenAI disclosed that two of its models—GPT-5.6 Sol and an unreleased, apparently more capable one—broke out of the sandbox they were being evaluated in, reached the open Internet, and compromised Hugging Face’s production infrastructure. Their apparent goal was to steal the answers to ExploitGym, an offensive-security benchmark built by outside researchers that…
Formal guarantees about programs come with fine print: they are only as solid as the assumptions and mechanisms behind them. Formal robustness guarantees about neural networks are no exception. Much of my recent work seeks to understand how those guarantees can be undermined, and what it takes to make them solid, as described in my Verified Certified Robustness series of posts. That series…
This post is the sixth in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent papers A Formally Verified Robustness Certifier for Neural Networks that appeared at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The…
This post is the fifth in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent papers A Formally Verified Robustness Certifier for Neural Networks that appeared at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The…
For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle. The triangle captures a trade-off between three desirable properties: Automation – the verification tool runs largely without human guidance Scalability – the technique works on large real systems Precision – the method can prove interesting properties,…
This post is a quick introduction to a concept that I have been using in talks since 2015, to help explain the landscape of formal verification methods and the inherent trade-offs between them. I originally came up with it as a way to contextualise my research to folks outside the formal methods community. However, it may have value beyond that. Formal methods, and the methods for verifying…
Note: this post was heavily updated on March 22, 2026 with the inclusion of the counterexamples against the adversarially-biased MNIST model. It was updated again on July 14, 2026: the counterexample numbers throughout now match the latest version of our paper, in which counterexamples are judged against a fully IEEE-754-compliant execution of each model (see the aside on execution semantics…
This post is the third in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent paper A Formally Verified Robustness Certifier for Neural Networks that will appear at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The…
This post is the second in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent paper A Formally Verified Robustness Certifier for Neural Networks that will appear at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate.…
This post is the first in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent paper A Formally Verified Robustness Certifier for Neural Networks that will appear at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate. The…
There has been much heat and light written in the wake of (what is now being called) SignalGate. I, myself, wrote in The Conversation about what this incident teaches us about the dangers of shadow IT, and the need for usable security. But this post is not primarily about that. Many people have noted that this incident was dangerous not because Signal was being used (as opposed to any other…
Douglas Adams famously quipped that we treat with skepticism any technology invented after our 35th birthday, but anything invented before is unremarkable. It happens that I joined University of Melbourne mere weeks after I turned 35. I am ashamed to say that up until that time (and for a little while after) I had been far too skeptical and dismissive towards machine learning research and…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…