Verified Trustworthy Software
The computing world is a wild west, with bugs in software the norm, and malicious people and hostile countries making use of them to attack people, companies and other nations. We can do better. Just as in the original wild west, advances have happened faster than law and order can keep up. Rather than catch cyber criminals we need to remove the possibility. In software the complexity of our computers and the programs they run has increased faster than ways have been developed and put in place to ensure they can be trusted. It is important that we can answer precisely questions such as “What does this code do?” and “Does it actually do what is intended?”, but can also assure ourselves of what code definitely does NOT do: it doesn’t include trapdoors for criminals to subvert, for example. Philippa Gardner has dedicated her working life to rectifying this by providing ways to verify software, so mathematically prove such trust-based properties hold of it.
Programs are incredibly complicated. Traditionally, software has been checked using testing. You run it on lots of input scenarios and check it does the right thing in those cases. If it does you assume it works in all the cases you didn’t have time to check. That is not good enough if you want code to really be trustworthy. It is impossible to check all possibilities, so testing alone is just not good enough. The only way to do it properly is to also use engineering methods based on mathematics. This is the case, not just for application programs, but also for the software systems they run within, and that includes programming languages themselves. If you can’t trust the programming language then you can’t trust any programs written in that language. Building on decades of work by both her own team and others, Philippa has helped provide tools and techniques that mean complex industrial software and the programming languages they are written in can now be verified mathematically to be correct. Helping secure the web is one area she is making a massive contribution via the W3C WebAssembly (Wasm) initiative. She is helping ensure that programs of the future that run over the web are trustworthy.
Programs written in programming languages are compiled (translated) into low level code (ie binary 1s and 0s) that can actually be run on a computer. Each kind of computer has its own binary instructions. Rather than write a compiler for every different machine, compilers often now use common intermediary languages. The idea is you have what is called a virtual machine – an imaginary one that does not really exist in hardware. You compile your code to run on the imaginary machine. A compiler is written for each language to compile it into the common low level language for that virtual machine. Then a separate, much simpler, translator can be written to convert that code into code for a particular real machine. That two step process is much easier than writing compilers for all combinations of languages and machines. It is also a good approach to make programs more trustworthy, as you can separately verify the separate, simpler parts. If programs compile to the virtual machine, then to be sure they cannot do harm (like overwrite areas of memory they shouldn’t be able to write to) you also only have to be sure that programs running on the virtual machine programs cannot , in general, do such harm.
The aim of Wasm is to make this all a reality for web programming, where visiting a web page may run a program you can’t trust. Wasm is a language with linked virtual machine that programming language compilers can be compiled into that itself will be trustworthy even when run over the web. It is based on a published formal specification of how the programming language and the virtual machine should behave.
As Philippa has pointed out, while some companies have good processes for ensuring their software is good enough, these are often kept secret. But given we all rely on such software we need much better assurances. Processes and tools need to be inspectable by anyone. That has been one of the areas she has focussed on. Working on Wasm is a way she has been doing that. Much of her work over 30 years or so has been around the development and use of logics that can be used to mathematically verify that concurrent programs are correct. Bringing that experience to Wasm has allowed her to work on the formal specification conducting proofs of properties of Wasm that show it is trustworthy in various way, correcting definitions in the specification when problems are found. Her approach is now being adopted as the way to do such checking.
Her work with Wasm continues but she has already made massive steps to helping ensure that the programs we use are safe and can be trusted. As a result, she was recently awarded the BCS Lovelace medal for her efforts.
More on …
Magazines …
Subscribe to be notified whenever we publish a new post to the CS4FN blog.
This blog and post is funded by EPSRC on research agreement EP/W033615/1.
cs4fn 