Lab 1: Verifying properties with Spin

Part 1: The dining philosophers

This assignment is about modeling the dining philosophers problem in Promela. A number of philosophers have gathered around a table to eat spaghetti. There are N philosophers around the table and N forks on the table. Philosophers are a very special breed and they need two forks to be able to eat. This means that they need to share forks with each other. When philosophers are not eating they like to busy themselves with some thinking. The picture to the right illustrates five philosophers sitting around a table with five forks.

Our model will contain philosophers modeled by Promela processes (with N specialized to 4):

#define N 4

proctype phil(int id) {
  do
    :: printf("thinking\n");
       /* ... */
       printf("eating\n");
       /* ... */
  od
}

init  {
  int i = 0;

  do
  :: i >= N -> break
  :: else -> run phil(i);
	     i++
  od
}

Task 1: Implementation

• The process needs to acquire one fork at a time. In particular, it is forbidden to acquire more than one fork inside a single atomic block.
• When both forks are acquired the philosopher eats and then puts the forks down again.
• The forks are a shared resource and should be modeled as such: any fork can be acquired by any adjacent philosopher. No other form of communication is allowed between the philosophers.

		Philosopher 3 is thinking
    Philosopher 0 is thinking
	Philosopher 1 is thinking
	    Philosopher 2 is thinking
	Philosopher 1 is eating with forks 1 and 0
	    Philosopher 2 is eating with forks 2 and 1
	Philosopher 1 is thinking
	    Philosopher 2 is thinking
		Philosopher 3 is eating with forks 3 and 2
	Philosopher 1 is eating with forks 1 and 0
		Philosopher 3 is thinking
	Philosopher 1 is thinking
	    Philosopher 2 is eating with forks 2 and 1
		Philosopher 3 is eating with forks 3 and 2

Task 2: Safety properties

1. Use assertions in your code to verify that a single fork cannot be held by more than one philosopher at any time. Fix your model if it does not satisfy this property.
2. Verify the same property using an LTL formula. Is your LTL solution equivalent to your assertion-based solution, or does one cover more than the other? If you discover new bugs, fix your model again.

Task 3: Liveness properties

1. Verify the absence of deadlocks in your model using Spin. Again, fix your model if this property is not satisfied. (The above safety properties must still hold after any fix.)
2. Formulate and verify one or more liveness properties about your model. At least one of your properties must guarantee that "something useful" happens infinitely often. Also, in your report, make sure to state how strong fairness assumptions you needed to prove your properties.
3. Explain why Spin cannot be used to prove starvation freedom for your model (that no philosopher ever starve).

Task 4: Reflection

This task is intentionally open-ended. What we expect from you is a short written reflection.

Recall what was said during the first lecture: One of the goals of applying formal methods is to increase your confidence in the correctness of specific software (and hardware) artifacts. After having completed the previous tasks, you have now formally verified your solution to the dining philosophers problem. Given this, how confident are you that your solution is correct? Would testing your solution using e.g. unit tests further increase your confidence? Would you be willing to bet a large sum of money on your solution being correct (if so, how much)? Lastly, mention two things (two risks) that could cause your result to be invalid; i.e., two things that could cause Spin to give incorrect answers to the questions you have provided to it.

Reporting part 1

Part 2: Needham-Schroeder protocol verification

Background: Security protocols

Public key cryptography

Most communication on the Internet and other networks is meant to be private. One way to achieve this is by using public key cryptography. Here, each principal X has published a public key pX, while keeping the corresponding secret key sX hidden from everybody else. Communication to X is encrypted under the public key pX, and can only be decrypted using the secret key sX.

Symmetric key encryption

Performing continuous encryption and decryption under public key cryptography is computationally expensive. To establish a faster communication channel one can use symmetric key cryptography. Here, a pair of principals shares the same key, which gives faster encryption and decryption (somehow; for details you have to take a course in cryptography). As a result, however, in a network of N principals, there must be N(N-1) unique shared keys.

Security protocols

One goal of security protocols is to get the best of both worlds. Using public key cryptography, two principals communicate two random numbers. If all steps in the protocol are executed correctly, it should be the case that

1. each principal has proven to be the person they claim to be (authenticity) and
2. only the involved principals know the communicated random numbers (confidentiality).

The communicated random numbers can be used to construct a symmetric (shared) key. Since no one else knows these numbers, subsequent communication can be encrypted under this shared key.

The Needham-Schroeder protocol

This assignment is about a famous security protocol: the Needham-Schroeder protocol. It is well-known for being vulnerable to an attack on both confidentiality and authenticity, and our goal is to find this attack using model checking. The protocol is as follows:

where

That is,

1. X sends to Y a message consisting of X's identity and a nonce encrypted under Y's public key.
2. Y's reply consists of X's nonce, proving that Y is the owner of the secret key, and Y's nonce, encrypted under X's public key. The nonces should now only be known to both principals, and can be used to construct a shared symmetric key (confidentiality).
3. Finally, X sends back Y's nonce, to prove that they have the right secret key (authenticity).

Modelling the network

Agents. Initially, our network consists of two agents: Alice, with public key kA, and Bob, with public key kB. The code below is a Promela model for Alice. It also contains supporting declarations for modelling encryption and the network.

Nonces. In a real system the nonces used in the actual protocol would be random numbers used only once. To keep the model simple and the state space small, nonces are modeled as names nonceA and nonceB. Keep the following in mind when dealing with nonces:

• Initially, only A knows nonceA, and only B knows nonceB.
• Any other agent we introduce does not know any nonces a priori.
• A nonce may only be learned by receiving/intercepting a message containing the nonce, while also being able to decrypt the message.

Messages. To represent encrypted messages we use a record Crypt that contains three entries: a key and two data entries (dubbed content1 and content2). With such representation encryption is modelled as creating a variable of type Crypt, where the key is the public key of the receiver. Therefore, decryption can only be done by matching the key entry with the key in possession of the agent.

Network. The network is modelled as a single message channel shared by all agents on the network. For simplicity, we use synchronous communication on the network, which is indicated by a buffer length of 0. While this does not affect the possible communication patterns, it helps to reduce the size of the model. A message on the network is a triple consisting of an identification tag (the message number), the intended receiver, and an "encrypted" message body.

Verification aids. For verification purposes we also introduce global variables partnerA, partnerB, statusA, statusB (ghost variables). The variable partnerA specifies who is Alice's intended partner. Similarly, partnerB indicates who is Bob's partner. In the beginning we explicitly set partnerA = agentB.

mtype = {ok, err, msg1, msg2, msg3, keyA, keyB, agentA, agentB,
	 nonceA, nonceB };

typedef Crypt { mtype key, content1, content2 };

chan network = [0] of {mtype, /* msg# */
		       mtype, /* receiver */
		       Crypt
};

/* global variables for verification*/
mtype partnerA, partnerB;
mtype statusA = err;
mtype statusB = err;

/* Agent (A)lice */
active proctype Alice() {
  /* local variables */

  mtype pkey;      /* the other agent's public key                 */
  mtype pnonce;    /* nonce that we receive from the other agent   */
  Crypt messageAB; /* our encrypted message to the other party     */
  Crypt data;      /* received encrypted message                   */


  /* Initialization  */

  partnerA = agentB;
  pkey     = keyB;

  /* Prepare the first message */

  messageAB.key = pkey;
  messageAB.content1 = agentA;
  messageAB.content2 = nonceA;

  /* Send the first message to the other party */

  network ! msg1 (partnerA, messageAB);

  /* Wait for an answer. Observe that we are pattern-matching on the
     messages that start with msg2 and agentA, that is, we block until 
     we see a message with values msg2 and agentA as the first and second  
     components. The third component is copied to the variable data. */

  network ? (msg2, agentA, data);

  /* We proceed only if the key field of the data matches keyA and the
     received nonce is the one that we have sent earlier; block
     otherwise.  */

  (data.key == keyA) && (data.content1 == nonceA);

  /* Obtain Bob's nonce */

  pnonce = data.content2;

  /* Prepare the last message */
  messageAB.key = pkey;
  messageAB.content1 = pnonce;
  messageAB.content2 = 0;  /* content2 is not used in the last message,
                              just set it to 0 */


  /* Send the prepared messaage */
  network ! msg3 (partnerA, messageAB);


  /* and last - update the auxilary status variable */
  statusA = ok;
}

active proctype Bob() {
   printf("placeholder for Bob\n")
}

Task 1: Write a model for Bob

Write a model for Bob that communicates with Alice's. In the official protocol, the principal identifier in the first message (X) is used by Bob to determine with who he is communicating, but we simplify this to Bob always assuming it is Alice who initalizes communication. Hence we always have:

partnerB = agentA;
pkey     = keyA;

Run the simulation with your implementation of Bob. As a last command in your model for Bob add a statement

statusB = ok;

Task 2: Spin

In this simple two-agent world everything should run smoothly and both Alice and Bob should always be able to reach the last statements in their corresponding models. In fact, this can be verified this with a temporal logic formula saying that eventually we reach a state where both statusA and statusB are ok.

Verify this property with a temporal logic formula in Spin.

ltl task2 { ... }

Task 3: Introducing the attacker

To study security guarantees of our protocol we investigate how communication between Alice and Bob is affected in the presence of a third agent: Intruder. The listing below presents an intruder process.

First, we extend declarations of possible agents, keys, nonces and agents to include the one for the attacker.

mtype = {... , agentI, keyI, nonceI } 

The code for the intruder then looks as follows:

active proctype Intruder() {
  mtype msg, recpt;
  Crypt data, intercepted;
  do
    :: network ? (msg, _, data) ->
       if /* perhaps store the message */
	 :: intercepted.key   = data.key;
	    intercepted.content1 = data.content1;
	    intercepted.content2 = data.content2;
	 :: skip;
       fi ;

    :: /* Replay or send a message */
       if /* choose message type */
	 :: msg = msg1;
	 :: msg = msg2;
	 :: msg = msg3;
       fi ;
       if /* choose a recepient */
	 :: recpt = agentA;
	 :: recpt = agentB;
       fi ;
       if /* replay intercepted message or assemble it */
	 :: data.key    = intercepted.key;
	    data.content1  = intercepted.content1;
	    data.content2  = intercepted.content2;
	 :: if /* assemble content1 */
	      :: data.content1 = agentA;
	      :: data.content1 = agentB;
	      :: data.content1 = agentI;
	      :: data.content1 = nonceI;
	    fi ;
	    if /* assemble key */
	      :: data.key = keyA;
	      :: data.key = keyB;
	      :: data.key = keyI;
	    fi ;
	    data.content2 = nonceI;
       fi ;
      network ! msg (recpt, data);
  od
}

1. Add the above code to your model and simulate it.
2. With the introduction of the intruder, the property from task 2 is no longer true. Find a counterexample with Spin and explain the cause of the failure.

Task 4: New assumptions on the attacker

In task 3 the intruder is a complete outsider. In this task we strengthen our assumptions about the intruder: not only can our attacker intercept and replay messages, but now they can also be a valid recipient of messages from Alice. That is, Alice may decide to start a communication with the intruder. Effectively, this corresponds to the intruder being a legitimate user of a system -- an insider with malicious intentions.

For this task, do the following:

1. Modify the code for Alice, so that she nondeterministically chooses either Bob or Intruder as her communication partner for her run of the protocol. The result of this choice should be reflected in the variable partnerA.
2. Once this choice is made, subsequent protocol messages should be encrypted with the key of the corresponding principal: with keyB when partnerA is agentB, and keyI when partnerA is agentI.

Task 5: Extending the Intruder

Now that the intruder may receive messages encrypted with their key, they should be able to decrypt and access the content of those (and only those) messages. Extend the intruder process to reflect this. Add two more ghost global variables that represent the attacker's knowledge of the nonces:

/* global variables for verification */
...
bool knows_nonceA, knows_nonceB;

Initialize these variables to false. In your modified code for the intruder, you will have to set these variables to true only when successful decryption of an intercepted message yields nonceA or nonceB. To add the possibility of decryption extend the intruder with another if block which checks the key of the intercepted data. If the key matches with the one of the intruder, proceed to check the content; skip otherwise.

When assembling content of the message that the intruder sends, use the variables knows_nonceA and knows_nonceB so that if these variables are true then the attacker may use the corresponding nonce. (To avoid potential spurious counterexamples.)

Moreover, to sligtly reduce nondeterminism in your model you may introduce "typing" for the intruder's messages. That is, if intruder is composing msg3 then content2 (which is not used for messages of type msg3) of the assembled message could be just set to 0. If you do this, consider also formally verifying that your modification actually decreases the amount of nondeterminism in your program (as a sanity-check).

Task 6: Attack

At this step your implementation should be ready to analyze security guarantees of our protocol. The following three properties specify the properties of the protocol:

propAB: If both Alice and Bob reach the end of their runs (i.e. both statusA and statusB are ok) then Alice's communication partner is Bob, and Bob's communication partner is Alice.

propA: If agent A reaches the end of its run (statusA is ok) and A believes it is talking to B (partnerA is agentB) then the intruder does not know A's nonce (!knows_nonceA).

propB: Similarly for B's nonce. That is: if agent B reaches the end of its run (statusB is ok) and it believes it is talking to A (partnerB is agentA) then the intruder does not know B's nonce (!knows_nonceB).

For this task, do the following:

1. Encode the above properties as temporal logic formulas and use Spin to verify them.
2. Since the protocol that we have presented is buggy, you should be able to find counterexamples to one or more of these properties. Which of the properties are violated? Explain what happens in your counterexample(s).

Task 7: Patching the protocol

There is a well-known patch to the protocol: in the patched version the second message of the protocol

is replaced with a message that contains the identity of principal Y:

For this task, do the following:

1. Modify your model to implement the patch.
2. Re-verify that your new model satisfies the three properties from task 6.

Task 8: Reflection

We again (as in part 1) ask you to reflect on your solution, but this time we only ask of you how confident you are in your solution. Having carried out formal verification, are you now 100 % sure that the protocol you have implemented is, in fact, safe?

Reporting part 2

Reporting

• See respective sections of part 1 and part 2
• Do not submit your files as an archive file (such as zip, tar.bz2, tar.gz or similar)
• Make sure to submit the reports in plain text format (.txt). Avoid other formats as this may cause delays in grading your submission.
• Submit via Fire

References

• Spin reference card (PDF)

Attributions

The dining philosophers image is created by Benjamin D. Esham and is licensed under the Creative Commons Attribution-Share Alike 3.0 Unported license.