Formal Methods for Software Development | TDA294/DIT271, LP1, HT2020 | ||||||||||||||||||||||||
Lab 1: Verifying properties with SpinPart 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: ImplementationYour first task is to implement the philosopher processphil according to these
rules:
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
Task 3: Liveness properties
Task 4: ReflectionThis 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.
Reporting part 1For part 1 of the assignment we expect:
Additional requirements:
Part 2: Needham-Schroeder protocol verificationBackground: Security protocolsPublic 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
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 protocolThis 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,
Modelling the networkAgents. 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:
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 BobWrite 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 whom 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: SpinIn 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 { ... }
Report:
Task 3: Introducing the attackerTo 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 }For this task, do the following:
Report:
Task 4: New assumptions on the attackerIn 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:
Task 5: Extending the IntruderNow 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 the 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: AttackAt 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:
Report:
Task 7: Patching the protocolThere 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:
Report:
Task 8: ReflectionWe 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 2For part 2 of the assignment we expect the collection of files from each task:
Additional requirements:
Reporting
References
AttributionsThe dining philosophers image is created by Benjamin D. Esham and is licensed under the Creative Commons Attribution-Share Alike 3.0 Unported license. | |||||||||||||||||||||||||
W. Ahrendt, Sep 9, 2019 |