How Can You Prove That Your Communication Is Secure?
Imagine a future election where voting can be done on-line. As a voter, you want to be sure that your vote safely arrives at the voting station, that it won't be modified on its way there, and that nobody can see how you vote. The voting station, on the other hand, wants to be sure that you only vote once. There will be rules for how the communication between you and the voting station is supposed to work. This set of rules is called a protocol. You want this protocol to be secure, but how can you be sure that it is?
Normally, a protocol is implemented in some programming language. Common programming languages (Java, C++, Visual-Basic, etc.) are not usually very well suited for reasoning about the things written in them, and therefore we need to create a model of the protocol and try to reason about the model instead. A model is a smaller and simplified version of the protocol, just like model railroads are smaller and simplified versions of real railroads. There exist a number of other "languages" that can be used to create a model, and these formal languages are better suited for reasoning about the things written in them. These languages are, in most cases, designed for reasoning about properties other than security properties, but some of them have been extended to deal with security, and these are the ones I will be working with. I will study these languages and try to find ways to use them and/or extend them to verify security properties for protocols, i.e. authenticity (Are you sure the sender of a message is who you think it is?) and confidentiality (Are you sure nobody else has seen what you just received?).
Formal languages can be translated into mathematical entities that are even better for reasoning. Using mathematics to reason about computer systems and protocols is called using "formal methods," and is a subfield within the field of computer science. Formal methods have thus far been mostly used to prove that safety critical systems are safe, for example railway switching and control. Little work has gone into verifying that computer systems are secure. I will try to develop ways to verify security properties for concurrent (parallel) systems, and create a set of tools that use my findings in order to automatically make this verification.
One of the main obstacles I will face is the classic problem of formal methods, referred to as "state space explosion." When a protocol (or a model of a protocol) is run, it can be in different states, depending on, for example, how long it has run, what the participants have communicated, and so on. For example, the "protocol" for saying hello in everyday life can be described as:
1. Person A says hello.
This protocol can be in three states: no one has said hello (that is, the protocol is in its initial state), one has said hello, or both have said hello (the final state). The set of all possible states is the state space. When you want to prove that a property holds for a protocol, you will have to check that the property holds in all states. A property you want to hold for the voting example is that no matter in which state the protocol for the voting is in, no one other than yourself knows how you vote (confidentiality). The problem is that there is usually a very large number of possible states, or, maybe even more common, that there are an infinite number of states. This large number of states is the reason the problem is called the state space explosion problem. Previous research has found a number of ways to decrease the number of states, and I will most likely be using one of them.
In the end I hope that my work will increase the confidence in electronic communication and computer systems. A lot of people (including myself) are very skeptical to doing more than the simplest bank errands on the Internet. Formal methods will lead to more robust and secure systems to the benefit of all.
|Modified 15 January 2003 * Contact Us|