264 lines
8.4 KiB
Alloy
264 lines
8.4 KiB
Alloy
|
|
// Names of you and your partner:
|
|
// FILL IN HERE
|
|
|
|
// the type of addresses
|
|
abstract sig Address {}
|
|
|
|
// some addresses are controlled by potential attackers
|
|
sig AttackerAddress extends Address {}
|
|
|
|
// one address belongs to the User who we model in this file
|
|
one sig UserAddress extends Address {}
|
|
|
|
// the four message types used in the protocol
|
|
abstract sig MessageType {}
|
|
one sig SDPOffer, SDPAnswer, SDPCandidates, Connect
|
|
extends MessageType {}
|
|
|
|
// a message has a type, plus a source (sender) and
|
|
// destination (receiver) addresses
|
|
sig Message {
|
|
type : MessageType,
|
|
source: Address,
|
|
dest : Address,
|
|
}
|
|
|
|
|
|
// the seven recorded call states
|
|
// SignallingOffered, SignallingOngoing are used only by the caller
|
|
// SignallingStart, SignallingAnswered, and Answered are used by the
|
|
// callee
|
|
// SignallingComplete is used by both caller and callee
|
|
abstract sig CallState {}
|
|
one sig SignallingStart, SignallingOffered, SignallingAnswered,
|
|
SignallingOngoing,
|
|
SignallingComplete, Answered, Connected
|
|
extends CallState {}
|
|
|
|
|
|
/* caller callee
|
|
------ ------
|
|
---- SDPOffer --->
|
|
SignallingOffered
|
|
SignallingStart
|
|
<--- SDPAnswer ----
|
|
SignallingAnswered
|
|
SignallingOngoing
|
|
---- SDPCandidates --->
|
|
SignallingComplete
|
|
SignallingComplete
|
|
------ ringing >>
|
|
<<--- user answers
|
|
Answered
|
|
<---- Connect -------
|
|
audio connected
|
|
audio connected
|
|
|
|
*/
|
|
|
|
// the state of the system
|
|
one sig State {
|
|
var ringing: lone Address, // whether the User is ringing and if so for whicih caller
|
|
var calls: Address -> lone CallState, // the recorded call state for each call currently in progress
|
|
var audio: lone Address, // the participant that the User's audio is connected to
|
|
var last_answered: lone Address, // the last caller the User answered a call from
|
|
var last_called: lone Address, // the last callee that the User called
|
|
var network: lone Message // the network, records the most recent message sent
|
|
}
|
|
|
|
|
|
// precondition for the User to send a message m in state s
|
|
pred user_send_pre[m : Message] {
|
|
m.source in UserAddress and
|
|
(
|
|
(m.type in SDPOffer and m.dest = State.last_called and no State.calls[m.dest]) or
|
|
(m.type in SDPAnswer and State.calls[m.dest] = SignallingStart) or
|
|
(m.type in SDPCandidates and State.calls[m.dest] = SignallingOngoing) or
|
|
(m.type in Connect and State.calls[m.dest] = Answered and
|
|
State.last_answered = m.dest)
|
|
)
|
|
}
|
|
|
|
// precondition for the User to receive a message m in state s
|
|
pred user_recv_pre[m : Message] {
|
|
m in State.network and
|
|
m.dest in UserAddress and
|
|
(
|
|
(m.type in SDPOffer and no State.calls[m.source]) or
|
|
(m.type in SDPAnswer and State.calls[m.source] = SignallingOffered) or
|
|
(m.type in SDPCandidates and State.calls[m.source] = SignallingAnswered) or
|
|
(m.type in Connect
|
|
and State.calls[m.source] = SignallingComplete)
|
|
)
|
|
}
|
|
|
|
// postcondition for the user sending a message m.
|
|
// s is the state the message is sent in and s' is the state
|
|
// after sending the message
|
|
pred user_send_post[m : Message] {
|
|
State.network' = m and
|
|
((m.type in SDPOffer and
|
|
State.calls' = State.calls + (m.dest -> SignallingOffered) and
|
|
State.ringing' = State.ringing and
|
|
State.audio' = State.audio) or
|
|
(m.type in SDPAnswer and
|
|
State.calls' = State.calls ++ (m.dest -> SignallingAnswered) and
|
|
State.ringing' = State.ringing and
|
|
State.audio' = State.audio) or
|
|
(m.type in SDPCandidates and
|
|
State.calls' = State.calls ++ (m.dest -> SignallingComplete) and
|
|
State.ringing' = State.ringing and
|
|
State.audio' = State.audio) or
|
|
(m.type in Connect and
|
|
State.calls' = State.calls and
|
|
State.ringing' = State.ringing and
|
|
State.audio' = m.dest)
|
|
)
|
|
}
|
|
|
|
|
|
// postcondition for the user receiving a message m
|
|
// s is the state before the message was received; s'
|
|
// is hte state after the message was received
|
|
//
|
|
// No need to specify here that last_called and last_answered to not change
|
|
pred user_recv_post[m : Message] {
|
|
no State.network' and
|
|
// Task 1.1: FILL IN HERE
|
|
}
|
|
|
|
// the action of the attacker sending a message
|
|
// s is the state before the message is sent, s' is the state after
|
|
pred attacker_msg {
|
|
some m : Message | m.source in AttackerAddress and
|
|
State.network' = m and
|
|
State.calls' = State.calls and
|
|
State.audio' = State.audio and
|
|
State.ringing' = State.ringing and
|
|
State.last_called' = State.last_called and
|
|
State.last_answered' = State.last_answered
|
|
}
|
|
|
|
// the action of the user either sending or receiving a message
|
|
pred user_msg {
|
|
State.last_answered' = State.last_answered and
|
|
State.last_called' = State.last_called and
|
|
some m : Message |
|
|
(user_send_pre[m] and user_send_post[m]) or
|
|
(user_recv_pre[m] and user_recv_post[m])
|
|
}
|
|
|
|
// the action of the user deciding to answer a ringing call
|
|
// doing so removes the "ringing" information from the state
|
|
// and changes the recorded call state to Answered but otherwise
|
|
// does not modify anything
|
|
pred user_answers {
|
|
some caller : Address |
|
|
State.calls[caller] in SignallingComplete and
|
|
State.ringing = caller and
|
|
State.audio' = State.audio and
|
|
no State.ringing' and
|
|
State.calls' = State.calls ++ (caller -> Answered) and
|
|
State.last_answered' = caller and
|
|
State.last_called' = State.last_called and
|
|
State.network' = State.network
|
|
}
|
|
|
|
// teh action of the user deciding to call another participant
|
|
// doing so simply updates the last_called state and also cancels
|
|
// any current "ringing" state
|
|
pred user_calls {
|
|
some callee : Address | State.last_called' = callee and
|
|
State.network' = State.network and
|
|
State.calls' = State.calls and
|
|
State.last_answered' = State.last_answered and
|
|
State.audio' = State.audio and
|
|
no State.ringing' // calling somebody else stops any current ringing call
|
|
}
|
|
|
|
pred state_unchanged {
|
|
State.network' = State.network
|
|
State.calls' = State.calls
|
|
State.last_answered' = State.last_answered
|
|
State.last_called' = State.last_called
|
|
State.ringing' = State.ringing
|
|
State.audio' = State.audio
|
|
}
|
|
|
|
// a state transition is either the user sending or receiving a msg
|
|
// or answering a call, or choosing to call somebody, or the attacker
|
|
// sending a message on the network
|
|
pred state_transition {
|
|
user_msg or user_answers or
|
|
attacker_msg or user_calls
|
|
or state_unchanged
|
|
}
|
|
|
|
// defines the initial state
|
|
// purposefully allow starting in a state where the User already
|
|
// wants to call somebody
|
|
pred init {
|
|
no State.audio and no State.ringing and
|
|
no State.last_answered and
|
|
no State.network and
|
|
all dest : Address | no State.calls[dest]
|
|
}
|
|
|
|
fact {
|
|
init
|
|
}
|
|
|
|
fact {
|
|
always state_transition
|
|
}
|
|
|
|
|
|
// a bad state is one in which the User's audio is connected
|
|
// to a participant but the User has not yet decided to call that
|
|
// participant or to answer a call from them
|
|
assert no_bad_states {
|
|
// Task 1.2: FILL IN HERE
|
|
}
|
|
|
|
// describe the vulnerability that this check identified
|
|
// The markers will reverse the "fix" to your model that you
|
|
// implemented and then run this "check" to make sure the vulnerability
|
|
// can be seen as described here.
|
|
// Task 1.3: FILL IN HERE
|
|
check no_bad_states
|
|
|
|
// Choose a suitable bound for this check to show hwo the
|
|
// vulnerability does not arise in your fixed protocol
|
|
// Justify / explain your choice of your bound and
|
|
// specifically, what guarantees you think are provided by this check.
|
|
// Task 2.2: FILL IN HERE
|
|
// See the assignment handout for more details here.
|
|
check no_bad_states // Task 2.2: CHOOSE BOUND HERE
|
|
|
|
|
|
|
|
// Task 3 example: a successful run in which a call is made by user
|
|
pred successful_run {
|
|
some other : Address | (always no State.calls.SignallingStart) and
|
|
eventually State.audio = other
|
|
}
|
|
// shows successful run of the protocol in the caller mode
|
|
run successful_run for 2 but 6 Message, 1..7 steps expect 1
|
|
|
|
pred successful_run2 {
|
|
// Task 3.1: FILL IN HERE
|
|
}
|
|
|
|
assert equivalent {
|
|
// Task 3.2: FILL IN HERE
|
|
}
|
|
check equivalent // Task 3.2: CHOOSE BOUND HERE
|
|
|
|
pred two_rings {
|
|
// Task 3.3: FILL IN HERE
|
|
}
|
|
run two_rings // Task 3.3: CHOOSE BOUND HERE
|
|
|
|
|