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.
Magic tricks are just algorithms – they involve a magician following the steps of the trick precisely. But how can a magician be sure a trick will definitely work when they do it in front of an audience? Just like computer scientists who can prove their algorithms always work, a magician can use logic and deduction to be sure their tricks always work too.
Image from Pixabay
Try the following trick on your own first, before reading about how it works or trying it with a volunteer. Take the role of both the magician and volunteer. I will do my best to remote-control the magic via my own mind-meld with you as you read my words, to try and make sure it works for you!
The magical effect
Take a full pack of playing cards and give them a good shuffle. Fan the cards face down. Now ask a volunteer to think of the colour RED and point to a card. Cut the pack at that point and count the top eight cards into a pile face down. Now ask them to think BLACK and touch another card. Cut the pack there and count out 7 cards onto the pile. Repeat this with 6 cards and then 5 cards having them think RED and then BLACK. Have the volunteer shuffle the selected cards then turn the pile face up.
Image by Paul Curzon
You take the cards that are left and shuffle them, keeping them face down. Have the volunteer now run through their cards taking out groups of cards that are together and of the same colour. They should put them either in a “RED” pile in front of them if they are a group of red cards, or in a “BLACK” pile if they are black, telling you how many cards they have placed in that pile. As they take each group of cards, you, focussing hard on your cards, but without looking at what they are, pick out the same number of cards from points through the pack as the volunteer put down, and put them in your own corresponding “RED” or “BLACK” pile in front of you, Place your cards face down. In this way, they end up with a pile of red cards and a pile of black cards, both face up in front of them. You end up with two corresponding face down piles in front of you. They have seen their cards but yours contain cards that you have not seen. Once they have run out of cards and you have placed your matching cards, stop and think for a moment, then go through your two piles and swap two cards without looking at them, saying you believe you made a couple of mistakes and those two ended up in the wrong piles.
Now, looking happy, tell the volunteer that through a mind-meld between you, them and the red and black cards you have, you believe, succeeded in your aim. Remind them that the piles were shuffled, they were responsible for the way the cards were split which was at random, and you haven’t seen any of your cards. One card out at any point and the trick would not have worked. Despite this, announce that you have managed to place the same number of red cards in your red pile as you have placed black cards in your black pile. Pass them the two piles in turn and ask them to check by first counting the red cards in your face down “RED” pile onto the table, and then do the same with the black cards that are in your “BLACK” pile.
Amazingly you have succeeded, the number of red cards in the red pile is the same as the number of black cards in the black pile.
Proving it always works
Did I mind meld with you to make it work? Or is something else going on? We can actually use logic and deduction (with some algebra) to show it works.
First we need to make a mathematical model of the situation – essentially describe the situation, or at least the parts of it that matter, in maths. That sounds a bit scary but it isn’t really. Its just giving names to some piles of cards! Let’s go through it…
In the trick, we end up with four piles of cards. A RED pile and a BLACK pile, both face up, in front of the volunteer and a RED pile and a BLACK pile, both face down, in front of the magician (see the picture above). We do not know how many cards are in each pile and it will be different each time we do the trick anyway because of all the shuffling. Luckily the actual numbers don’t matter. In the trick we care about the numbers of red cards and the numbers of black cards, Let us therefore use mathematical variables to represent these different numbers (that just means give them names!). Mathematicians often use names like x and y for variables, but to help us remember what they stand for we will use variations on R and B to mean numbers of red and black cards respectively.
So, we will use R to stand for the number of red cards in the volunteer’s face up “RED” pile (which are all red) and B to mean the number of black cards in the volunteers face up “BLACK” pile (which are all black).
Now for the magician’s face down piles. They have both red and black cards in each pile so we will write R1 to mean the number of red cards in the magician’s face down “RED” pile and B1 to mean the number of black cards in the magician’s face down “RED” pile. Similarly, we will write R2 to mean the number of red cards in the magician’s face down “BLACK” pile and B2 to mean the number of black cards in the magician’s face down “BLACK” pile. We have the situation as shown below in the picture..
Image by Paul Curzon
In doing this we are doing a form of abstraction – hiding of detail – we have hidden the actual numbers of red and black cards in each pile within our description, describing them with variables as the precise numbers do not matter (and are different every time we do the trick anyway).
So far so good. Now, we want to try and prove that the trick always works. But how to start? First, just think of any facts you know about the situation (and especially anything you know about red and black cards). It may not be obvious how it can help, but write it down anyway!
Well the first thing we know is that a full pack of cards was used, and there are 52 cards in a pack, half (26) red and half (26) black. All these cards ended up on the table in one pile or another. So that means if we add up all the red cards in the four piles it will equal 26. How can we write this in terms of our variables? It is just:
R + R1 + R2 = 26
We add the three variables that stand for numbers of red cards and it equals 26. There are only three things to add for the four piles as one pile is all black. We can say a similar thing about the black cards:
B + B1 + B2 = 26
Now we have two different sums that equal the same thing (26) so we can put them together as equalling each other to get a combined equation which we will call EQUATION 1.
R + R1 + R2 = B + B1 + B2 (EQUATION 1)
That doesn’t seem to tell us much useful, but don’t worry, we are just gathering facts for now. What else do we know about how the trick worked? Well, every time the volunteer put some number of cards in their “RED” pile, the magician puts the same number of cards in their “RED” pile (though those cards may be red or black). That means that, throughout the two “RED” piles hold the same number of cards. The number of cards in one “RED” pile is R and the number of cards in the other “RED” pile is R1 + B1 (the reds plus the blacks in that pile). We can write this out as an equation:
R = R1 + B1
Now, this tells us that R is exactly the same as R1 + B1 so anywhere we see R we can replace it with R1 + B1. In particular, we can make this switch in EQUATION 1 to give:
(R1 + B1) + R1 + R2 = B + B1 + B2 (EQUATION 2)
With the same logical reasoning, we can deduce an equation for the “BLACK” piles too. The number of cards in one “BLACK” pile is B and the number of cards in the other “BLACK” pile is R2 + B2 (the reds plus the blacks in that pile). We can write this out as an equation:
B = R2 + B2
Substituting R2 + B2 for B into EQUATION 2 we get EQUATION 3
Now, this seems to have just made things more complicated and not got us anywhere much, but we can now simplify it. Notice that there are two R1s on one side and two B2s on the other, each added, so we can group them together to get:
2R1 + B1 + R2 = R2 + 2B2 + B1
Also, on each side there is a B1 and that pair can cancel out (just subtract B1 from both sides and the equality holds but it is simpler), and on each side there is an R2 which can cancel in the same way. This leaves us with:
2R1 = 2B2
Of course the multiplication by 2 on both sides cancels too (just divide both sides by 2 and they will still be equal). We get:
R1 = B2
That is a very simple equation. It basically tells us that if you follow the steps of this trick that, whatever numbers of reds and blacks end up in each pile, R1 is guaranteed at the end to be the same number as B2. So what does that mean back in the real world? R1 just stands for the number of red cards in the magician’s “RED” pile. B2 just stands for the number of black cards in the magician’s “BLACK” pile. The equation we are left with just tells us that as long as we follow the steps (actually as long as we make the number of cards in each pair of piles match) then at the end the number of red cards in the magician’s “RED” pile will be the same as the number of black cards in the magician’s “BLACK” pile…and that is the “magical” result we predicted!
The trick will always work if you follow the steps!
Proving software and hardware always works
A magic trick involves the magician following steps precisely – following an algorithm. That is all computer hardware and software do – they follow algorithms to achieve some desired result (a magical effect). Just as we proved the trick always works, we can prove that other algorithms (whether implemented as a program or hardware) work using logical deduction too. That is one of the reasons why logic and deduction are so important to computer scientists. You do not want a trick to go wrong in front of an audience, so it is worth proving it always works. How much more important is it that all that software we now rely on for everyday life is error free. And what about a medical device keeping someone alive, or the software flying a plane. We want to be sure they always work. If they contain mistakes, people die. Logic and proof can therefore save lives, not just magic shows.
The truth table for NOT P. A yellow brick represents P. Blue means True and Red means false. Read along the rows to get the meaning of NOT P when P is true or false. Image by CS4FN
We have seen how to represent truth tables in lego. Truth tables are a way of giving precise meaning to logical operations like AND, OR and NOT. They are also give a way to do logical reasoning following a simple algorithm.
That’s Not Not True
You may have been pulled up in English and told you just said the opposite of what you meant, after saying something like “There ain’t no way I’m doing that”. This is a “double negative” as the “n’t” in “ain’t” is really “not” so followed by “no way” you are actually saying “not not way” or overall: “I am doing that”. Perhaps the most famous double negative is in the Rolling Stones song “(I can’t get no) satisfaction”. English is very flexible though and double negatives like this don’t cancel out but just become a different way of saying the negative version. In logic two negations do cancel out, though. Let’s take a purer version to work with: the statement “I am not not happy”. What does this mean? In logic the basic proposition here is “I am not happy”. The logical statement is “NOT (NOT (I am happy))”.
We can prove what this means using truth tables. We can do more than just prove what this single statement means. We can prove what all double negatives mean, more generally. We do this by replacing the proposition “I am happy” with a variable P. It now becomes NOT (NOT P) or in our lego version where we use a yellow brick to mean a proposition, P:
Image by CS4FN
This is just syntax, just a sequence of symbols. It doesn’t give us any meaning on its own. We can build truth tables in Lego for that. We start from the variables that are at the inside of the logical expression which here is just the variable P. We list in a table column the possible values it can take (true or false).
Image by CS4FN
This shows P (yellow) can be either be TRUE (blue) or FALSE (red). Now we build up the logical expression of interest a column at a time. NOT is applied to P, so we add a new column for NOT P and use the truth table for the operator, NOT, to tell us what lego brick to put in each row based on the lego brick already there. The NOT truth table is at the top of the page. It says if you have a blue brick in a row, place a red brick there. If you have a red brick, put a blue brick there. This gives us a new filled out column for (NOT P) which is just a copy of the NOT truth table (but bare with us that was just a simple case). We get:
Image by CS4FN
Moving outwards in the expression NOT (NOT P)), we now look at the operator applied to (NOT P). It is NOT again. We add a new column to our truth table and again use the NOT truth table to work out the new values, but this time applied to the column before (the NOT P column). The NOT truth table says put a blue brick for a red brick, and a red brick for a blue brick in the column it is being applied to (the NOT P column). This gives:
Image by CS4FN
The result is a truth table with coloured bricks identical to that of the original column for P. Switching back from lego bricks to what the columns mean, we have shown that the NOT(NOT P) column is the same as the P column, or in other words that NOT(NOT P) EQUALS P (whatever value P has).
We can actually go a step further though, because equivalence is just a logical operation with its own truth table. It gives true if the two operands have the same value and false otherwise (or in lego terms if the bricks are the same colour the answer is a blue brick and if they are different colours the answer is a red brick. The truth table looks like this:
Image by CS4FN
We can use this truth table to calculate whether two lego truth table columns are equal or not just by looking up the combinations in this EQUALS truth table. Continuing our example we can carrying building our truth table about NOT(NOT P)). To make things clearer first add a column corresponding to P again. That means we will be applying the EQUALS operator to the last two columns. As before, for each row, look up the corresponding pattern for those last two columns in the EQUALS truth table to get the answer for that row. In the first row we have two blue bricks so that becomes a blue brick according tot he EQUALS truth table. In the next row we have two red bricks. That also becomes a blue brick. This gives:
Image by CS4FN
The thing to notice here is that all the entries in the final answer column are blue lego pieces. Switching back from the lego world to the logic world, what does this mean? Blue is true so all rows in the answer are true. That means whatever value of the proposition P the answer to NOT (NOT P) EQUALS P is true. We have proved a theorem that this is always true. We have shown by building with lego that a double negation cancels itself out.
Logical expressions like this that are always true (whatever the values of the variables) are called tautologies. We can tell something is a tautology, so we have proved a theorem, just by the simple manual check that its truth table values are true (or in lego all blue).
The important thing to realise about this is all the reasoning can be done without knowing what the symbols mean, and certainly not worrying about English words, once you have the truth tables. You do it mechanically. You do not need to think about what, for example, red and blue mean until the end. At that point you return to the logical world to see what you have found out. All blue means it is always true! You can also at that point substitute back in actual words of interest into the statements proved. P means “I am happy”. We started by asking what “I am not not happy” means. We converted this to “NOT (NOT (I am happy))”. By swapping in “I am happy” for P in our theorem gives us that NOT (NOT “I am happy”) EQUALS “I am happy”, or that “I am not not happy.” just means the same as “I am happy”
We have been reasoning about English statements, but this kind of reasoning is the basis of all logical reasoning and essentially the basis of formal verification where the meaning of programs and hardware is checked to see if it meets a specification. It tells you what a test in a program like “if (! temperature != 0) …) means so does for example, or what a circuit with two NOT gates does.
And lego logic has even given us a way to prove things just by building with lego.
Part of a series featuring featuring pixel puzzles, compression algorithms, number representation, gray code, binary, logic and computation.
EPSRC supports this blog through research grant EP/W033615/1, The Lego Computer Science post was originally funded by UKRI, through grant EP/K040251/2 held by Professor Ursula Martin, and forms part of a broader project on the development and impact of computing.
cs4fn 