The Great Story Teller: Byzantine Armies, Part-Time Parliaments, And Spending More Time Thinking

The Great Story Teller: Byzantine Armies, Part-Time Parliaments, And Spending More Time Thinking

Yesterday, I was writing some code, and my latest Macbook Pro with its advanced ARM architecture froze. Basically, (I think) it had run out of memory but didn’t tell me about it, and it just decided to give up, and stop.

So, here we are in the 21st Century and with 10s of gigabit per second network speeds, and we can’t even design a computer system that doesn’t crash on a regular basis. And, when these types of things happen, I think of Leslie Lamport’s work and in his dedication to solving real-life problems with real-life solutions. Luckily, he’s still doing interviews, and you can read his current thinking here.

Leslie has been cited over 80,300 times and has an h-index of 83 (meaning that he has 83 papers which have 83 or more citations). But perhaps a key indicator of his outputs is that his i10-index is 189 (which defines that he has 189 research papers with more than 10 citations). Some of his top papers are [here]:

Pushing the boundaries of what is possible

In our modern digital world, we take too many things for granted. We have almost lost the ability to read maps anymore, as we have the magic of GPS at our fingertips. But, the work on GPS took decades of solid research to get it to the point, that you can almost instantly find out where you are in the world, and easily track your steps. But, we don’t even see it as a feature in our smartphones … it is just there. In the eyes of those who created GPS, it must still be a wonder, but in the eyes of our next generation, it’s just there.

And the resilience of our modern systems was basically formed from the research work of the 1970s and 1980s. And one person who was way ahead of anyone else: Leslie Lamport. His contribution has been so great, that on 18 March 2013, he received the AM Turing Award (which is like a Nobel Prize in Computer Science). At the time, Bill Gates said:

Leslie has done great things not just for the field of computer science, but also in helping make the world a safer place. Countless people around the world benefit from his work without ever hearing his name. … Leslie is a fantastic example of what can happen when the world’s brightest minds are encouraged to push the boundaries of what’s possible.

Leslie sole-authored many great papers. His most cited work relates to time, clocks and distributed systems and which currently has 13,233 citations [3] (and which grows by the day):

Designing a house without a blueprint

Leslie has continually focused on two major problems within the creation of software that often occur: the lack of formal verification; and the lack of a formal design. For him, there’s a disconnect between those who teach formal verification of systems and those who teach programming. For Leslie, those who teach formal verification can often lack real-life practice and implementation skills, but those who teach programming can sometimes have little idea about how to verify their code formally.

And, so we are stuck with a Catch-22 situation, where we too often see developers race to create their code, without ever thinking about its formal verification for its correctness. So many major projects thus fail to deliver what they have been expected to deliver as there is often little thought given to the solution and how it will be verified by both the client and the customer.

In his most recent paper [1], he outlines that we perhaps spend too long just creating code and that we should perhaps focus on “Finding a better solution by thinking about the problem and its solution, rather than just thinking about the code”. His analogy is that you wouldn’t build a house without a blueprint.

But, of course, software lives a privileged life, and where we have allowed it: to crash; have security weaknesses; and be riddled with bugs — in a way that would be almost unacceptable with any other area of our lives. Imagine if your car froze randomly while waiting at traffic lights and that you had to press a big button on the dashboard for a few seconds, and have it rebooted each time? Overall, we would send the car back to the dealer and ask for another one. But for software, we just accept that it has bugs, struggles to run on hardware, and has probably not been tested properly.

To address this problem, Lamport created a specification language known as TLA+ (Temporal Logic of Actions) [2] — which creates a high-level representation of a system and can formally verify its correctness.

The Part-Time Parliament

But, the great thing about Leslie is that he never quite did things in the normal academic way. For one, we typically sole-authored his papers and thus did not rely on PhD students to source his ideas. As the number of authors increases by the day, it is great to read a paper that is solely the work of the author. These perhaps lead to papers which have more purpose and focus, and are consistent in their approach. They also better define the person who actually did the work.

His papers, too, are often self-contained little gems, which contained a core focus on a major problem, then define these as use cases based on real-life problems, and followed by the formal methods which could be implemented by others. The great thing was that when reading the paper, it was not always apparent that the problem existed. And so reviewers perhaps struggled a bit — in the same way, they perhaps struggled with Ralph Merkle’s groundbreaking work.

In most of the papers, engineers were guided through a step-by-step approach that gave them full solutions to the problems that he prosed. Leslie was not the type to give a small contribution to one part of the problem — he went in a solved a whole lot of things — and then waited for others to catch up.

One of his most interesting papers was “The Part-Time Parliament” which outlined the Paxos method. In fact, it got forgotten about in the review process, and was published many years after it was initially proposed [4][5]:

In the paper, he moved away from the normal approach of defining the mathematical approach but instead tells a story around the island of Paxos. The story involves a number of legislators, and where each would record a sequence of decrees, but these ledgers could then be inconsistent in their recording. For example, if one legislator (Λ˘ινχ∂) recorded:

37: Painting on temple walls is forbidden

and another (Φισ∂ρ) missed these decree and recorded a conflicting one of:

37: Freedom of artistic expression is guaranteed

But, you must smile when you find out that all the actors in the use case have names which are made up of Greek symbols, and where the Cheese inspector has the name of ∆˘ικστρα:

The method is known as the Paxos family of consensus algorithms.

LaTeX

One of Leslie’s amazing contributions was LaTeX [6], and its original manual was published in 1986:

Leslie, at the time, worked for the much missed Digital Equipment Corporation (DEC). Overall, DEC had a strong focus on microcomputers and in using the UNIX operating system. To Leslie, creating a document was a bit like creating a program, and it needed an editor, an operating system and a compiler. The source content could then exist within any system and didn’t need a special program to read it. To convert the source content into the end document, it just required a compiler, and which could check for problems. To change something in the formatting; it then just required a recompilation.

Unfortunately, Microsoft Word took off with its easy-to-use GUI, but it had an overblown user interface. Its style and content became intertwined, and where it is often difficult to change document formats. It also had binary formatting of content and basically locked-in many users. The move from DOC to DOCX further complicated things, as a change in a single character, leads to a completed different binary file. But, LaTeX is still the only proper way to inherently share documents in a neutral form, and in separating the presentation from the content. And while Microsoft Word has changed little over the years, LaTeX continues to advance, and with the advent of GitHub and Overleaf, we have ways of sharing documents in a way that avoids lock-in.

Clocks

Many researchers think that the quality measure of a paper relates to the impact factor of the journal it is submitted to or in the amount of maths it contains. But, in the end, it is the impact of the paper, and how it changes thinking. So, in 1978, Leslie published a paper on clocks and that changed the scientific world. It is now one of the most cited papers in computer science [here]:

Byzantine Generals Problem

After the success of the clock’s paper, in 1981, Leslie B Lamport defined the Byzantine Generals Problem [here]:

And, in a research world where you can have 100s of references in a paper, Leslie only used four (and which would probably not be accepted these days for having so few references):

Within this paper, the generals of a Byzantine army have to agree to their battle plan, in the face of adversaries passing in order information. In the end, we aim to create a way of passing messages where if at least two out of three of the generals are honest, we will end up with the correct battle plan.

So, why don’t we build computer systems like this, and where we support failures in parts of the system, or where parts of the system may be taken over for malicious purposes? And the answer is … no reason. We are stuck with our 1970s viewpoint of the computing world, where everything works perfectly, and security is someone else’s problem to fix.

We may thus have a system where we create a number of trusted nodes to perform a computation, and then have an election process at the end to see if we have a consensus for a result. So, if we have three generals (Bob, Alice and Eve), we need two of them to be honest, which means we can cope with one of our generals turning bad:

In this case, Eve could try and sway Trent by sending the wrong command, but Bob and Alice will build a better consensus, and where Trent will go with them. The work could then be defined as MPC (Multiparty Computation) and where we have multiple nodes getting involved to produce the final result. In many cases, this result could just be as simple as a Yes or No, and as to whether a Bitcoin transaction is real or fake, or whether an IoT device has a certain voltage reading.

The Lamport Signature

Shor’s algorithm [here] has shown that we can break our existing public key methods on quantum computers. One method to replace these methods is to use hash-based signatures, and it was Leslie who produced the first hash-based signature method [here] that is still in use today:

Here is the work referenced within the SPHINCS+ paper:

When we sign a message we take its hash and then encrypt it with our private key. The public key is then used to prove it and will prove that we signed it with our private key. The Lamport signature uses 512 random hashes for the private key, and which are split into Set A and Set B. The public key is the hash of each of these values. The private key size is 16KB (2×256×256 bits) and the public key size is also 16 KB (512 hashes with each of 256 bits).

The basic method of creating a Lamport hash signature is:

• We create two data sets with 256 random 256-bit numbers (Set A and Set B). These are the private key (512 values).
• Next, we take the hash of each of the random numbers. This will give 512 hashes and will be the public key.
• We then hash the message using SHA-256 and then test each bit of the hash (0 … 255). If it is a 0, we use the ith number in Set A, else we use the ith number from Set B.
• The signature is then 256 random numbers (taken from either Set A or Set B) and the public key is the 512 hashes (of Set A and Set B).

This process is illustrated below:

We can use the Lamport method for one-time signing, but, in its core format, we would need a new public key for each signing. The major problem with Lamport is thus that we can only sign once with each public key. We can overcome this, though, by creating a hash tree which is a merger of many public keys into a single root. A sample run which just shows the first few private keys and the first public keys:

==== Private key (keep secret) =====
Priv[0][0] (SetA):  6f74f11f20953dc91af94e15b7df9ae00ef0ab55eb08900db03ebdf06d59556c
Priv[0][1] (SetB):   4b1012fc5669b45672e4ab4b659a6202dd56646371a258429ccc91cdbcf09619
Priv[1][0] (SetA):  19f0f71e913ca999a23e152edfe2ca3a94f9869ba973651a4b2cea3915e36721
Priv[1][1] (SetB):   04b05e62cc5201cafc2db9577570bf7d28c77e923610ad74a1377d64a993097e
Priv[2][0] (SetA):  15ef65eda3ee872f56c150a5eeecff8abd0457408357f2126d5d97b58fc3f24e
Priv[2][1] (SetB):   8b5e7513075ce3fbea71fbec9b7a1d43d049af613aa79c6f89c7671ab8921073
Priv[3][0] (SetA):  1c408e62f4c44d73a2fff722e6d6115bc614439fff02e410b127c8beeaa94346
Priv[3][1] (SetB):   e9dcbdd63d53a1cfc4c23ccd55ce008d5a71e31803ed05e78b174a0cbaf43887
==== Public key (show everyone)=====
Pub[0][0]:  7f2c9414db83444c586c83ceb29333c550bedfd760a4c9a22549d9b4f03e9ba9
Pub[0][1]:   4bc371f8b242fa479a20f5b6b15d36c2f07f7379f788ea36111ebfaa331190a3
Pub[1][0]:  663cda4de0bf16a4650d651fc9cb7680039838d0ccb59c4300411db06d2e4c20
Pub[1][1]:   1a853fde7387761b4ea22fed06fd5a1446c45b4be9a9d14f26e33d845dd9005f
==== Message to sign ===============
Message:	The quick brown fox jumps over the lazy dog
SHA-256:	d7a8fbb307d7809469ca9abcb0082e4f8d5651e46d3cdb762d02d0bf37c9e592
==== Signature =====================
Sign[0]:	4b1012fc5669b45672e4ab4b659a6202dd56646371a258429ccc91cdbcf09619
Sign[1]:	04b05e62cc5201cafc2db9577570bf7d28c77e923610ad74a1377d64a993097e
Sign[2]:	8b5e7513075ce3fbea71fbec9b7a1d43d049af613aa79c6f89c7671ab8921073
Sign[3]:	1c408e62f4c44d73a2fff722e6d6115bc614439fff02e410b127c8beeaa94346
The signature test is  True

In this case, we take the random number and then convert it to a string. So the SHA-256 signature of “6f74f11f20953dc91af94e15…0db03ebdf06d59556c” is 7f2c9414db83444c586c…49d9b4f03e9ba9. If can be seen that the hash of the message (“The quick brown fox jumps over the lazy dog”) has a hex D value at the start, which is 1101 in binary, and we see we take from SetB [0], SetB [1], SetA [2] and SetB [3]. A demonstration is given here.

Conclusions

And, there you go … be inspired that a single person can contribute more to our scientific and technical world than large and faceless corporations. Believe in the power of the human mind, and see the world for all its technological and scientific beauty. In a world that seems dominated by politicians and political parties, believe in the power of research to solve many of our real problems.

So go read some more about Leslie:

References

[1] Lamport, L. (2015). Who builds a house without drawing blueprints?. Communications of the ACM, 58(4), 38–41.

[2] Lamport, L. (1994). The temporal logic of actions. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(3), 872–923.

[3] Lamport, L. (2019). Time, clocks, and the ordering of events in a distributed system. In Concurrency: the Works of Leslie Lamport (pp. 179–196).

[4] Lamport, L. (2001). Paxos made simple. ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001), 51–58.

[5] Lamport, L. (2019). The part-time parliament. In Concurrency: the Works of Leslie Lamport (pp. 277-317).

[6] Lamport, L. (1985). I1 (\LaTeX) — -A Document (Vol. 410, p. 413). pub-AW.