Toby's Blog

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]