Deceptive Security
An important internet standard undergoes a revamp. There is zero room for error. The stakes couldn't be higher.
A researcher that has been pursuing an idea since his doctoral thesis and sticks to it even though his colleagues dismiss it as a gimmick.
Three doctoral students and a professor who dare the impossible to protect others.
And the crucial question of what can be done, what must be done, to ensure that the foundation of the internet is secure and remains secure.
All four stories are connected to one man. He has been living in Saarbrücken since 2018, does research and teaches at the CISPA Helmholtz Center for Information Security: Professor Cas Cremers.
At the age of ten, he sits in front of a computer for the first time. Unfortunately, the computer, a Philips MSX-2, is at a friend's house. Since his parents don't buy him one, he borrows a book about the BASIC programming language from the public library and devours it. Then a public broadcaster announces a programming competition. Eleven-year-old Cas solves the tasks with pencil on graph paper - and wins.
The main prize is not a computer, but a book about raising children. Title: "Fatherhood"
At 15, he founds the company "Parallax" to develop more games. A friend joins. Together they develop six computer games: Space pirates, wizards, robots. In all of them, the designer, composer and author is Cas.
After he has his A-levels in the bag, Cas wants to do less programming and learn more about the theory of computer science. He starts studying computer science in Eindhoven. After another year, he also enrols in philosophy at Tilburg University and starts an internet company. Although everything is going well, Cas realizes: it's too much.
Approximately five billion people [1] read, write, and play on the internet today. And this is with a world population of eight billion people [2] . Every second, they send packets of data through the network of networks.
Of course, online shopping is also an important factor.
The global revenue in e-commerce is estimated to reach as much as 5.9 trillion US dollars [3] in 2023.
To illustrate this figure: The Saarland, where CISPA is based, has an area of 2,570 square kilometers [4] .
If we were to cash out 5.9 trillion US dollars in 20-dollar bills, we would receive 295 billion banknotes.
With that, we could pave the entire area of Saarland once.
When we shop and make payments online, the online store, of course, communicates with our bank.
In this process, the security protocol "Transport Layer Security" (TLS) ensures that the transmitted data packets are encrypted.
TLS is just one of many protocols that our packets of data use to travel safely through the internet, ...
but it is the encrypted connection provided by TLS that enables ...
secure payment transactions and thus global online commerce.
This makes TLS one of the most important security protocols.
Transport Layer Security (TLS) is one of the most important security protocols on the Internet. Specified in 1999, it has been working along for seven years in 2015 under version number 1.2 [6] , protecting the integrity and confidentiality of online data. Over time, vulnerabilities are becoming apparent. TLS 1.2 urgently needs an update.
This has been the task of the international "Internet Engineering Taskforce", or IETF for short, since 1986. It is financed by donations, and its sponsors include technology companies such as Cisco, Ericsson, Huawei and Nokia. The IETF itself is an honorary organization of experts from science and industry. They discuss in working groups via publicly accessible mailing lists. They meet in person no more than three times a year. "We reject kings, presidents and voting. We believe in rough consensus and running code" [7] is their mantra.
The working group for the successor to TLS 1.2 is headed by Eric Rescorla, a Yale graduate, former security architect at Skype [8] and until June 2023 technical director for the Firefox Internet browser at the Mozilla Foundation in California, US. Rescorla has already written a book [9] about TLS and its predecessor SSL. Experts like Bruce Schneier praise it [10] . Rescorla is concerned. Just one single flaw in the specification of TLS 1.3 could bring the Internet to its knees. He is contacting researchers outside the IETF about it. One of those he has not even considered yet - Cas.
2015, a summer evening in Oxford. As a professor, Cas has resolved to pay more attention to his work-life balance. This doesn’t include answering emails late at night. But when the name Thyla Van Der Merve comes up, he doesn't hesitate. He already knows the doctoral student from the "Royal Holloway University of London". Van Der Merve is looking for the best software for a new, high-profile project. Seven emails and 90 minutes later, she has much more. A team has been formed.
Thyla Van Der Merve and her colleague Sam Scott are joined by Cas and his graduate student Marko Horvat. Together, the four of them dare to do what no one has done before: the formal verification of the full TLS 1.3 with all its components.
Ever since the "RMS Titanic" went down, we've known about the sneaky nature of icebergs: Out at sea, a significant portion of them remains hidden from view.
The same goes for internet surfing: Whether we're ordering books online, listening to music tracks on our smartphones via an internet connection, or even downloading them, the most crucial processes take place in the depths of technology.
Before we even get to see a single image or read any text, our own devices have already exchanged messages with computers. Everything works together like gears in a well-oiled machine. However, even a small mistake can bring an entire program or service to a halt. Suddenly, all warning lights turn red.
Formal verification aims to prevent this.
The beauty of formal verification lies in its ability to guarantee what testing can only give hope for: Programs and protocols function without errors.
Formal verification replaces hope with proof.
The drawback: Formal verification is highly demanding. It requires a precise mathematical definition of the behavior of the program or protocol under scrutiny. This so-called specification needs to be mathematically proven.
In light of this, the renowned British computer scientist Sir Tony Hoare called for the development of software tools that can "automatically verify programs to the extent possible"
[11]
. He referred to the development of such a tool as "a grand challenge for computing research"
[12]
.
Formally verified software is like a mathematical proof: Every statement logically follows from the preceding one. As a result, each line of code, and every computation path described by it, must be mathematically proven.
Anyone familiar with the Hoare calculus knows how challenging it is to formally verify a program by this means, even if it consists of only a few lines.
Nowadays, programs and protocols range from thousands up to several hundred thousand lines.
Anyone who takes on the challenge of formal verification will soon find themselves in a maze-like garden without boundaries. Formal verification overwhelms us humans.
We need assistance.
Computers! They trade on the stock market, defeat chess grandmasters, and win quiz shows. Their computational power and speed surpass us humans.Can they take over the task of formal verification?
Unfortunately, computers don't recognize that a meter-long toothbrush is nonsense. They also don't think of freezing boiling water to have clear ice cubes instead of cloudy ones in their glass.
They lack both the understanding of our real world and the ability to think outside the box. However, formal verification precisely demands that.
Hence, humans and computers must collaborate, letting their strengths interlock like gears and compensate for each other’s weaknesses.
Computer and human form the
"Team Formal Verification"
.
By now, not only technology giants like NVIDIA [13] and Microsoft [14] utilize formal verification. Other companies in hardware and software development have also embraced its use.
Another reason for this uptake is the internet: It intensifies the impact of errors in software and protocols, much like gasoline accelerates a fire.
At CISPA, researchers are therefore expanding the use of formal verification to not only ensure the operational reliability of software and protocols but also guarantee their cybersecurity.
In this way, formal verification can tackle the intricacies of technology. No grinding gears, no more red warning lights, everything is in the green zone.
For icebergs, such a technology has not been found. Instead, their migration in the North Atlantic and Antarctica is monitored by aircraft and radar satellites. The International Ice Patrol issues warnings via email.
"If we don't find an attack, they'll say what you're doing is irrelevant and doesn't add value." Cas openly addresses the risk to Thyla, Sam and Marko. It's summer 2015, and the group is in the early stages of the project. Cas knows the skepticism of other scientists. People have already expressed their doubts to him during his time in Zurich. He is also worried about the PhD students' careers. If they don't discover a security hole, they will just waste precious time instead of advancing their doctoral theses. Cas decides
[15]
: They won't regret it.
A new security protocol is in the making. Experts study it carefully and point their thumbs up or down
[16]
. That's how reviews looked so far. However, Cas and the others want to guarantee the security of TLS 1.3 by means of mathematical proofs. An important tool for this is software that can provide such proofs. Experts call these programs "provers".
The researchers are relying on a prover for which Cas already had initial ideas during his doctoral thesis and which he developed together with Simon Meier, Benedikt Schmidt and Professor David Basin in Zurich. As he did during his game development days, Cas is taking on other roles. He looks for a name that works in several languages, is not a swear word, not an abbreviation. Cas takes inspiration from animals and comes across a monkey with a white mustache. He proposes the monkey's face as a logo, its subgenus as part of the name, and "Tamarin Prover" [17] is born.
Tamarin Prover analyzes whether the steps of a security protocol are secure or can be exploited by an attacker. The program can check protocols with complex procedures and many people or endpoints involved. Considering the rapid development of the Internet, such a comprehensive analysis is indispensable.
Tamarin Prover acts like an investigator at a crime scene. It follows traces and checks which ones lead to a perpetrator. Its tools are not magnifying glasses and fingerprint brushes, but mathematical methods. If the software has worked through all the tracks and has not encountered an attacker, the protocol is secure. Q.E.D.
Attack found
No attack found
Thyla and Sam are doing their internship at the Mozilla Foundation in California, USA, supervised by Eric Rescorla. They are trying to become acquainted with the Tamarin Prover. They are working through the PhD theses written about the Prover, extracting everything that will help them understand the tool from the ground up. Marko is in Oxford and always just a Skype call away. He gives them crash courses, including examples for finite automata and basic security protocols. After a few weeks, Thyla and Sam can experiment with the prover independently of Marko. They also make tremendous progress with formal verification. They are ready for TLS 1.3.
To enable the Tamarin Prover to screen TLS 1.3, the software needs three pieces of the puzzle in advance.
Sam, Thyla, and Marko specify what the imaginary attacker can do. They decide on an old acquaintance. It can control the entire network, infiltrate, intercept, modify and delete messages. Its name has been in the relevant research literature for years: "Dolev-Yao".
Then they discuss long and often to decide what security conditions TLS 1.3 must meet.
These too they write in a so-called .spthy file for the Tamarin Prover.
In the meantime, the IETF's experts are moving forward with the design of TLS 1.3. They are producing minimalist text. The PhD students are glad that this is available at least digitally so that they can search it. Their task is to translate the communication steps of the protocol described in English into a language that the Tamarin Prover understands. They are building a model.
For the Tamarin Prover each protocol step is translated. You can imagine each protocol step as a domino.
A protocol consists of many steps.
The Tamarin Prover attempts to link the protocol steps into a path.
If the software finds a path from the starting point to the attack, it is possible to gain access to confidential information. A security vulnerability exists.
Royal Holloway University of London, Department of Mathematics, McCrea Building, Room 255, Sam's desk is littered with printed out technical papers [18] . Eight graduate students sit in the office, which is about the size of a classroom. The workstations differ only in the books on the small shelves behind them. The subjects are category theory, geometry and cryptography. Sam is back in England. Time and again, the four researchers have incorporated design changes from the IETF into their model, being extremely careful to update every affected location in the code. They missed the luxury of a development environment for the Prover and made do with a macro processor. Three months into the project, all the preliminary work for the prover is done. The proving begins.
First the human thinks, then the Tamarin Prover computes.
The human analyzes the graph ...
... and draws conclusions on how the model needs to be modified.
The program searches for attacks. If it does not terminate, this may be due to various reasons.
That is why the Tamarin Prover represents the information flow of the protocol as a graph. It extends up to the stopping point.
The cycle repeats.
Tamarin Prover offers two ways to construct proofs. There is a fully automatic mode that combines logic and heuristics to find proofs. When the tool finishes the automatic proof search, there is either a correctness proof or a counterexample that allows an attack.
Since the correctness of security proofs is an undecidable problem, the Tamarin Prover sometimes cannot complete the proof. It then needs help, which it gets through its interactive mode. A human must check the proof states and go through the information flow, which the software visualizes as a graph. Manual reasoning is combined with automatic evidence search.
Of the four researchers, Sam is taking on this task. He has long felt the draw from basic research to applications. During his undergraduate studies at the University of Warwick, he studied mathematics, and when he started his doctoral thesis he worked on cryptography and number theory. Now provable security is his topic, and the Tamarin Prover is his sparring partner.
"Tamarin Prover can't really tell you what you've done wrong because, to the best of its knowledge, it only executes the protocol you've given it," Sam explains. That's why when the prover gets stuck or even marks an attack, Sam always checks the model of the protocol first. He looks to see if an argument, a parameter, or a variable has been forgotten somewhere. If he thinks he has fixed the error, he restarts the prover with the corrected model. Always a big help: The graphical user interface.
Since calculating the entire proof takes too much computing time, the four researchers divide the proof into 40 parts. With the help of over 100 small, self-written hints for the prover, so-called lemmas, they manage to get Tamarin Prover to prove 35 of the 40 automatically. Sam does the rest interactively with the Prover. They are Team Tamarin.
October 2015, it is evening. Again Sam sits in the open plan office at Royal Holloway, again his screen shows the graphical user interface of the Tamarin Prover. He clicks to prove lemmas. But the Tamarin Prover sticks to its red arrows. This is how the software says: Here's where the attacker can get information it never should. Again and again, Sam goes through the graph. Why doesn't the proof work? It's not because of the model. Sam is pretty confident [19] . He writes an email to the group and to Eric Rescorla, with whom he has been in contact since the Mozilla internship. To the email he attaches the image file with the huge graph. The subject of the late night email is, "Found something odd."
Two hours later. Eric Rescorla is the first to respond. It is an attack.
The next morning the team meets. According to Sam, the mood is neither crisis nor party, but focus. The group reviews the attack and immediately sets out to develop a countermeasure. Impressive in its complexity to even the best of hackers, they decide to close the security gap. They want to defuse the attack that would impress even hackers.The imaginary attacker has to send at least 18 network messages, combine three different mechanisms of TLS 1.3
[20]
, then he can slip into the identity of a victim and, for example, plunder his online money account, while the bank only perceives a legal transfer. Authentication is broken.
Again, the Tamarin Prover helps the group. One of the software's strengths is rapid prototyping. Again and again, Sam, Thyla, Marko and Cas let the Tamarin Prover run. This way, they get confirmation that their new solution is really secure. Then, just under a week later, on Saturday, October 31, 2015, at 12:35 a.m. local time, Sam announces the attack and the fix on the IETF mailing list
[21]
. Educational material for the experts. Q.E.D.
The graph for TLS 1.3: The Tamarin Prover allows an analysis at multiple levels of detail.
Academia and industry are now paying attention to the four researchers. Sam presents the results in January 2016 at the industry conference "Real World Crypto" in Stanford, California, Marko does so
[22]
at the world-famous conference "IEEE Symposium on Security & Privacy" a few months later. For all three PhD students, a large part of their doctoral thesis is now on TLS 1.3. They also write two technical papers, which to this day top their publication list in number of citations. Cas is even invited by Eric Rescorla to a meeting of the TLS working group at Mozilla's headquarters in California. A knightly accolade for the four of them and the Tamarin Prover.
Summer 2022.
The Tamarin Prover has already successfully investigated around 50 protocols
[23]
. Applications range from Wi-Fi to electronic payment to communication between power plants
[23]
.
Thyla is now a security engineering manager at Google in Zurich, Sam co-founded a startup called Oso in New York, and Marko teaches at the University of Zagreb.
Cas sits in his corner office on the second floor at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany. The interview about TLS 1.3 is coming to a close. "I'm sure they would never have discovered this attack," he says looking back, adding, "After more than ten years of experience, I can safely say that there's usually something to find."
When asked about the impact of formal verification of TLS 1.3, Eric Rescorla responds via email: „TLS 1.3 has served as a blueprint for future protocol work. Since then, in several cases formal verification helped us to find and eliminate potential serious defects.“
A few weeks after the interview. The parquet floor in CISPA's lecture hall smells of cleaning agent and the clock at the wall shows twenty to twelve. The last minutes of a lecture are running. "Real-world protocols" is the topic today. Cas is giving it. His arms, his hands, even his fingers are moving. They form imaginary spheres, paint circles, draw lines in the air. They frame, divide, count up. Even the feet join in. Cradle step, back and forth. Cas dances through his lecture. He's in his element.
CREDITS
Research & Text
- Gordon Bolduan
Visual Design
- Yushun Zhao
Motion Design
- Sascha Schäfer, Yushun Zhao
Web Development
- Sascha Schäfer
Project Management
- Georg Demme
Development Support
- Johannes Ebersold, Wolfgang Herget, Sebastian Weisgeber
User Research
- Sarah Cieslik
Special Thanks
Videography
- Tobias Ebelshäuser
Interviewees
- Cas Cremers, Niklas Medinger, Aurora Naska, Sam Scott