From d606c271f98426d47ffe28ed47a7104685c9222b Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 26 Nov 2024 15:56:41 +0100 Subject: [PATCH 01/22] Add MWE for proving SIF --- verification/scratch/mwe1.gobra | 244 ++++++++++++++++++++++++++++++++ 1 file changed, 244 insertions(+) create mode 100644 verification/scratch/mwe1.gobra diff --git a/verification/scratch/mwe1.gobra b/verification/scratch/mwe1.gobra new file mode 100644 index 000000000..f3c572ad8 --- /dev/null +++ b/verification/scratch/mwe1.gobra @@ -0,0 +1,244 @@ +// Minimal working example 1. Only implements very basic structure. +// 0. The key K is already given. +// 1. We receive a message M over the network. +// 2. We compute a "MAC tag" of M using K. +// 3. We send the computed tag over the network. +package mwe + +////////////////////////////// I/O Actions ////////////////////////////// +// cf. running-example/policy/actions.gobra + +// Definition of I/O actions (abstract, for trace). +type Action adt { + RecvIO{int} + SendIO{int} + // NOTE: I have left out `p` (cf. paper) for now + // It would be necessary once we have multiple options of which message to + // declassify at some point in order to make this deterministic in the + // previous I/O actions again. However, at the moment, our IOD spec only + // allows declassifying one message depending on the previous I/O actions + DeclassifyIO{int} +} + +// Extract input of I/O action. 0 signifies no input. +ghost +decreases +pure func (a Action) Input() int { + return match a { + case RecvIO{?m}: m + case SendIO{_}: 0 + case DeclassifyIO{_}: 0 + } +} + +// Extract output of I/O action. 0 signifies no output. +ghost +decreases +pure func (a Action) Output() int { + return match a { + case RecvIO{_}: 0 + case SendIO{?t}: t + case DeclassifyIO{?t}: t + } +} + +////////////////////////////// Classification spec. ////////////////////////////// +// cf. running-example/policy/classification.gobra +// cf. running-example/classifications/basic.gobra + +type ClassificationSpec interface { + ghost + decreases + pure Classification(Action) Specification +} + +// Gives universal access to the trace. +// `pure` ensures the resulting pointer always points to the same trace. +ghost +decreases +pure func History() *Trace + +type Trace adt { + Empty{} + Snoc{Trace;Action} // Snoc: reverse cons +} + +type Specification adt { + Spec{Observation;Observation} +} + +type Observation adt { + Value{int} // NOTE: eventually might want to switch back to any + None{} + Some{Observation} + Tuple{Observation;Observation} +} + +type ObservationTrace adt { + EmptyObs{} + SnocObs{InitObs ObservationTrace;Observation} +} + +// The following is our assertion language. +ghost +decreases +pure func True() Observation { + return None{} +} + +ghost +decreases +pure func Low(v int) Observation { + return Value{v} +} + +// Given that all sensitivity preconditions have been satisfied in the trace, +// this allows us to assume that the sensitivity postconditions are satisfied. +ghost +decreases +requires acc(History(), 1/2) && low(Pre(sig,*History())) +ensures acc(History(), 1/2) && low(Post(sig,*History())) +func LowPost(sig ClassificationSpec) + +type Collect domain { + func Post(ClassificationSpec, Trace) ObservationTrace + func Pre(ClassificationSpec, Trace) ObservationTrace + func pre_(Specification) Observation + func post_(Specification) Observation + + // NOTE: these are the low projections mentioned in the paper + axiom { + (forall p,q Observation :: {pre_(Spec{p,q})} pre_(Spec{p,q}) == p) && + (forall p,q Observation :: {post_(Spec{p,q})} post_(Spec{p,q}) == q) + } + + axiom { + (forall sig ClassificationSpec :: {Post(sig,Empty{})} Post(sig,Empty{}) == EmptyObs{}) && + (forall sig ClassificationSpec :: {Pre(sig,Empty{})} Pre(sig,Empty{}) == EmptyObs{}) && + (forall sig ClassificationSpec, t Trace, e Action :: {Post(sig,Snoc{t,e})} Post(sig,Snoc{t,e}) == SnocObs{Post(sig,t), post_(sig.Classification(e))}) && + (forall sig ClassificationSpec, t Trace, e Action :: {Pre(sig,Snoc{t,e})} Pre(sig,Snoc{t,e}) == SnocObs{Pre(sig,t), pre_(sig.Classification(e))}) + } +} + +type DefaultClassification struct {} + +ghost +decreases +pure func (DefaultClassification) Classification(a Action) Specification { + return match a { + case DeclassifyIO{?t}: Spec{True(), Low(t)} // Make `t` low. + case _: Spec{Low(a.Output()), Low(a.Input())} + } +} + +////////////////////////////// I/O spec. ////////////////////////////// +// cf. running-example/policy/iodspec.gobra + +// We express the IODSpec as a (IOD-)guarded transition system. +type IODSpec interface { + // `Guard` specifies which I/O actions may be taken, depending on the + // (content of) the action (in particular, not on the sensitivity). + ghost + decreases + pure Guard(state, Action) bool + + ghost + decreases + pure Update(state, Action) state +} + +type Restriction domain { + func IsTrace(IODSpec, Trace) bool + func Reaches(IODSpec, Trace, state) bool + + axiom { + forall r IODSpec, t Trace, s state, a Action :: { Snoc{t, a}, Reaches(r, t, s) } Reaches(r, t, s) && r.Guard(s, a) ==> Reaches(r, Snoc{t, a}, r.Update(s, a)) + } + + axiom { + forall r IODSpec, t Trace, s state :: {Reaches(r, t, s)} Reaches(r, t, s) ==> IsTrace(r,t) + } +} + +// Our I/O spec. The state is the private key and the most recently received message. +type MWE1 struct {} + +type state struct { + key int + lastMsg int +} + +// We allow send, recv to happen at any point. +// Declassify can only be called on a MAC tag of the most recently received message +// generated with the private key. +ghost +decreases +pure func (MWE1) Guard(s state, a Action) bool { + return match a { + // NOTE: This makess our IOD spec well-formed, as what is allowed to be + // declassified is now deterministic in the previous I/O actions. + case DeclassifyIO{?t}: t == MAC(s.key, s.lastMsg) + case _: true + } +} + +ghost +decreases +pure func (MWE1) Update(s state, a Action) state { + return match a { + case RecvIO{?m}: state { key: s.key, lastMsg: m } + case _: s + } +} + +////////////////////////////// Trusted library I/O ////////////////////////////// +// cf. running-example/library/library.gobra + +// Receive message `m` over network. +decreases +requires acc(History()) +ensures acc(History()) && *History() == Snoc{old(*History()), RecvIO{m}} +func Recv() (m int) + +// Send tag `t` over network. +decreases +requires acc(History()) +ensures acc(History()) && *History() == Snoc{old(*History()), SendIO{t}} +func Send(t int) + +// Declassify tag `t`. +ghost +decreases +requires acc(History()) +ensures acc(History()) && *History() == Snoc{old(*History()), DeclassifyIO{t}} +func Declassify(t int) + + +////////////////////////////// Program ////////////////////////////// + +// Abstract function representing the computation of a MAC. +// key x message -> MAC tag +decreases +pure func MAC(int, int) int + +// Receives a message, authenticates it using a MAC, and sends the resulting tag. +// The state `s` contains the private key of this router, +// and the most recently received message. +// NOTE: it should suffice here to just require Reaches(...) after the program +// has terminated, bc. at the moment we definitely terminate and there is no way +// to violate the I/O spec. and "undo" this violation later on (-> safety property). +// TODO: in the future, we should probably check this after every I/O action instead? +// In the original example, I think this is done via the shared invariant. +preserves acc(History()) && acc(s) && low(Pre(DefaultClassification{}, *History())) && Reaches(MWE1{}, *History(), *s) +func authenticate(ghost s *state) { + m := Recv() + LowPost(DefaultClassification{}) + ghost s.lastMsg = m + + t := MAC(s.key, m) + + /* ghost */ Declassify(t) + /* ghost */ LowPost(DefaultClassification{}) + Send(t) + /* ghost */ LowPost(DefaultClassification{}) +} \ No newline at end of file From f5603b6a76422924712c447d7f01758876cacd6e Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 9 Dec 2024 11:17:01 +0100 Subject: [PATCH 02/22] Add MWE2 --- verification/scratch/{ => mwe1}/mwe1.gobra | 2 +- verification/scratch/mwe2/mwe2.gobra | 132 +++++++++++++++++++++ 2 files changed, 133 insertions(+), 1 deletion(-) rename verification/scratch/{ => mwe1}/mwe1.gobra (99%) create mode 100644 verification/scratch/mwe2/mwe2.gobra diff --git a/verification/scratch/mwe1.gobra b/verification/scratch/mwe1/mwe1.gobra similarity index 99% rename from verification/scratch/mwe1.gobra rename to verification/scratch/mwe1/mwe1.gobra index f3c572ad8..4b8e49984 100644 --- a/verification/scratch/mwe1.gobra +++ b/verification/scratch/mwe1/mwe1.gobra @@ -3,7 +3,7 @@ // 1. We receive a message M over the network. // 2. We compute a "MAC tag" of M using K. // 3. We send the computed tag over the network. -package mwe +package mwe1 ////////////////////////////// I/O Actions ////////////////////////////// // cf. running-example/policy/actions.gobra diff --git a/verification/scratch/mwe2/mwe2.gobra b/verification/scratch/mwe2/mwe2.gobra new file mode 100644 index 000000000..8f1a1297f --- /dev/null +++ b/verification/scratch/mwe2/mwe2.gobra @@ -0,0 +1,132 @@ +// Minimal working example 2. +package mwe2 + +// Used to track position in protocol. +type Place int +pred token(ghost p Place) + +pred RecvPerm(ghost p Place) + +// Returns the next place after calling `Recv` from `p`. +// Avoids using an existential quantifier. +ghost +requires RecvPerm(p) +decreases +pure func Recv_T(ghost p Place) Place + +// Used to refer to the received message. +ghost +requires RecvPerm(p) +decreases +pure func Recv_R(ghost p Place) int + +// This is how the state is/should be updated after receiving message `m`. +decreases +pure func Recv_S(s state, m int) state { + return state { key: s.key, lastMsg1: m, lastMsg2: s.lastMsg1, lastMsg3: s.lastMsg2 } +} + +requires token(p) && RecvPerm(p) +ensures token(old(Recv_T(p))) +ensures m == old(Recv_R(p)) +ensures low(m) +func Recv(ghost p Place) (m int) + +pred SendPerm(ghost p Place, t int) + +ghost +requires SendPerm(p, t) +decreases +pure func Send_T(ghost p Place, t int) Place + +requires token(p) && SendPerm(p, t) +requires low(t) +ensures token(old(Send_T(p, t))) +func Send(ghost p Place, t int) + +pred DeclassifyPerm(ghost p Place, tag int, t int) + +ghost +requires DeclassifyPerm(p, tag, t) +decreases +pure func Declassify_T(ghost p Place, tag int, t int) Place + +// In order to make permitted declassifications deterministic in low data, +// we add low parameter `p` to "tag" declassifications. +// (Necessary as otherwise IOD spec Protocol2 would not be well-formed.) +ghost +requires token(p) && DeclassifyPerm(p, tag, t) +requires low(tag) +ensures token(old(Declassify_T(p, tag, t))) +ensures low(t) +decreases +func Declassify(ghost p Place, tag int, t int) + +// "Linear" protocol. +pred Protocol1(ghost p Place, key int) { + // 1. Receive a message. + RecvPerm(p) && + // 2. Compute MAC tag and declassify it. + DeclassifyPerm(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))) && + // 3. Send MAC tag over network. + SendPerm(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))) && + // 4. Restart. + Protocol1(Send_T(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))), key) +} + +type state struct { + key int // the private key + lastMsg1 int // 1st most recently received message + lastMsg2 int // 2nd + lastMsg3 int // 3rd +} + +pred Protocol2(ghost p Place, s state) { + // Receive a message at any time. + RecvPerm(p) && Protocol2(Recv_T(p), Recv_S(s, Recv_R(p))) && + // NOTE: at the moment we can declassify things before receiving anything + // Declassify and send either the most or the 2nd most recently received message. + DeclassifyPerm(p, s.lastMsg1, MAC(s.key, s.lastMsg1)) && Protocol2(Declassify_T(p, s.lastMsg1, MAC(s.key, s.lastMsg1)), s) && + DeclassifyPerm(p, s.lastMsg2, MAC(s.key, s.lastMsg2)) && Protocol2(Declassify_T(p, s.lastMsg2, MAC(s.key, s.lastMsg2)), s) && + SendPerm(p, MAC(s.key, s.lastMsg1)) && Protocol2(Send_T(p, MAC(s.key, s.lastMsg1)), s) && + SendPerm(p, MAC(s.key, s.lastMsg2)) && Protocol2(Send_T(p, MAC(s.key, s.lastMsg2)), s) +} + +// Abstract function representing the computation of a MAC. +// key x message -> MAC tag +decreases +pure func MAC(int, int) int + +requires token(p0) && Protocol2(p0, s) +func authenticate(ghost p0 Place, s state) { + + invariant token(p0) && Protocol2(p0, s) + for { + unfold Protocol2(p0, s) + ghost p1 := Recv_T(p0) + m1 := Recv(p0) + s = Recv_S(s, m1) + + unfold Protocol2(p1, s) + ghost p2 := Recv_T(p1) + m2 := Recv(p1) + s = Recv_S(s, m2) + + unfold Protocol2(p2, s) + ghost p3 := Recv_T(p2) + m3 := Recv(p2) + s = Recv_S(s, m3) + + // We can use m2, m3 here. m1 won't work. + t := MAC(s.key, m3) + + unfold Protocol2(p3, s) + ghost p4 := Declassify_T(p3, m3, t) + Declassify(p3, m3, t) + + unfold Protocol2(p4, s) + ghost p0 = Send_T(p4, t) + Send(p4, t) + } + +} \ No newline at end of file From 9328a953930c68731548e6ca680151041e09953b Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 17 Dec 2024 14:55:43 +0100 Subject: [PATCH 03/22] Address PR feedback --- verification/scratch/mwe1/mwe1.gobra | 67 +++++++++++++++-------- verification/scratch/mwe2/mwe2.gobra | 79 +++++++++++++++------------- 2 files changed, 86 insertions(+), 60 deletions(-) diff --git a/verification/scratch/mwe1/mwe1.gobra b/verification/scratch/mwe1/mwe1.gobra index 4b8e49984..97d747383 100644 --- a/verification/scratch/mwe1/mwe1.gobra +++ b/verification/scratch/mwe1/mwe1.gobra @@ -3,7 +3,7 @@ // 1. We receive a message M over the network. // 2. We compute a "MAC tag" of M using K. // 3. We send the computed tag over the network. -package mwe1 +package mwe ////////////////////////////// I/O Actions ////////////////////////////// // cf. running-example/policy/actions.gobra @@ -96,27 +96,43 @@ pure func Low(v int) Observation { // this allows us to assume that the sensitivity postconditions are satisfied. ghost decreases -requires acc(History(), 1/2) && low(Pre(sig,*History())) -ensures acc(History(), 1/2) && low(Post(sig,*History())) +requires sig != nil && acc(History(), 1/2) && low(Pre(sig,*History())) +ensures acc(History(), 1/2) && low(Post(sig,*History())) func LowPost(sig ClassificationSpec) -type Collect domain { - func Post(ClassificationSpec, Trace) ObservationTrace - func Pre(ClassificationSpec, Trace) ObservationTrace - func pre_(Specification) Observation - func post_(Specification) Observation +// NOTE: these are the low projections mentioned in the paper +ghost +decreases +pure func pre_(spec Specification) Observation { + return match spec { + case Spec{?p, _}: p + } +} +ghost +decreases +pure func post_(spec Specification) Observation { + return match spec { + case Spec{_, ?q}: q + } +} - // NOTE: these are the low projections mentioned in the paper - axiom { - (forall p,q Observation :: {pre_(Spec{p,q})} pre_(Spec{p,q}) == p) && - (forall p,q Observation :: {post_(Spec{p,q})} post_(Spec{p,q}) == q) +ghost +decreases len(trace) +requires sig != nil +pure func Pre(sig ClassificationSpec, trace Trace) ObservationTrace { + return match trace { + case Empty{}: EmptyObs{} + case Snoc{?t, ?e}: SnocObs{Pre(sig, t), pre_(sig.Classification(e))} } +} - axiom { - (forall sig ClassificationSpec :: {Post(sig,Empty{})} Post(sig,Empty{}) == EmptyObs{}) && - (forall sig ClassificationSpec :: {Pre(sig,Empty{})} Pre(sig,Empty{}) == EmptyObs{}) && - (forall sig ClassificationSpec, t Trace, e Action :: {Post(sig,Snoc{t,e})} Post(sig,Snoc{t,e}) == SnocObs{Post(sig,t), post_(sig.Classification(e))}) && - (forall sig ClassificationSpec, t Trace, e Action :: {Pre(sig,Snoc{t,e})} Pre(sig,Snoc{t,e}) == SnocObs{Pre(sig,t), pre_(sig.Classification(e))}) +ghost +decreases len(trace) +requires sig != nil +pure func Post(sig ClassificationSpec, trace Trace) ObservationTrace { + return match trace { + case Empty{}: EmptyObs{} + case Snoc{?t, ?e}: SnocObs{Post(sig, t), post_(sig.Classification(e))} } } @@ -147,17 +163,13 @@ type IODSpec interface { pure Update(state, Action) state } +// NOTE: We don't need IsTrace but it is not clear how to translate Reaches. type Restriction domain { - func IsTrace(IODSpec, Trace) bool func Reaches(IODSpec, Trace, state) bool axiom { forall r IODSpec, t Trace, s state, a Action :: { Snoc{t, a}, Reaches(r, t, s) } Reaches(r, t, s) && r.Guard(s, a) ==> Reaches(r, Snoc{t, a}, r.Update(s, a)) } - - axiom { - forall r IODSpec, t Trace, s state :: {Reaches(r, t, s)} Reaches(r, t, s) ==> IsTrace(r,t) - } } // Our I/O spec. The state is the private key and the most recently received message. @@ -175,7 +187,7 @@ ghost decreases pure func (MWE1) Guard(s state, a Action) bool { return match a { - // NOTE: This makess our IOD spec well-formed, as what is allowed to be + // NOTE: This makes our IOD spec well-formed, as what is allowed to be // declassified is now deterministic in the previous I/O actions. case DeclassifyIO{?t}: t == MAC(s.key, s.lastMsg) case _: true @@ -231,6 +243,12 @@ pure func MAC(int, int) int // In the original example, I think this is done via the shared invariant. preserves acc(History()) && acc(s) && low(Pre(DefaultClassification{}, *History())) && Reaches(MWE1{}, *History(), *s) func authenticate(ghost s *state) { + // NOTE: forgetting the calls to either of `Declassify` and `LowPost` + // would result in a verification error *in the postcondition* (and not in + // the call to send), as here, compliance to the classification spec is + // not checked on every I/O call, but instead on the trace at the end of + // the function call. + m := Recv() LowPost(DefaultClassification{}) ghost s.lastMsg = m @@ -240,5 +258,8 @@ func authenticate(ghost s *state) { /* ghost */ Declassify(t) /* ghost */ LowPost(DefaultClassification{}) Send(t) + // The following call to `LowPost` is the only one not needed (here), + // as we don't need the postcondition of the last I/O call to verify + // the remainder of the function. /* ghost */ LowPost(DefaultClassification{}) } \ No newline at end of file diff --git a/verification/scratch/mwe2/mwe2.gobra b/verification/scratch/mwe2/mwe2.gobra index 8f1a1297f..477bdf79f 100644 --- a/verification/scratch/mwe2/mwe2.gobra +++ b/verification/scratch/mwe2/mwe2.gobra @@ -1,5 +1,5 @@ // Minimal working example 2. -package mwe2 +package mwe // Used to track position in protocol. type Place int @@ -10,13 +10,11 @@ pred RecvPerm(ghost p Place) // Returns the next place after calling `Recv` from `p`. // Avoids using an existential quantifier. ghost -requires RecvPerm(p) decreases pure func Recv_T(ghost p Place) Place // Used to refer to the received message. ghost -requires RecvPerm(p) decreases pure func Recv_R(ghost p Place) int @@ -27,51 +25,47 @@ pure func Recv_S(s state, m int) state { } requires token(p) && RecvPerm(p) -ensures token(old(Recv_T(p))) -ensures m == old(Recv_R(p)) +ensures token(next_p) && next_p == Recv_T(p) +ensures m == Recv_R(p) ensures low(m) -func Recv(ghost p Place) (m int) +func Recv(ghost p Place) (ghost next_p Place, m int) pred SendPerm(ghost p Place, t int) ghost -requires SendPerm(p, t) decreases pure func Send_T(ghost p Place, t int) Place requires token(p) && SendPerm(p, t) requires low(t) -ensures token(old(Send_T(p, t))) -func Send(ghost p Place, t int) +ensures token(next_p) && next_p == Send_T(p, t) +func Send(ghost p Place, t int) (ghost next_p Place) pred DeclassifyPerm(ghost p Place, tag int, t int) ghost -requires DeclassifyPerm(p, tag, t) decreases pure func Declassify_T(ghost p Place, tag int, t int) Place -// In order to make permitted declassifications deterministic in low data, -// we add low parameter `p` to "tag" declassifications. -// (Necessary as otherwise IOD spec Protocol2 would not be well-formed.) ghost requires token(p) && DeclassifyPerm(p, tag, t) requires low(tag) -ensures token(old(Declassify_T(p, tag, t))) +ensures token(next_p) && next_p == Declassify_T(p, tag, t) ensures low(t) decreases -func Declassify(ghost p Place, tag int, t int) +func Declassify(ghost p Place, tag int, t int) (ghost next_p Place) // "Linear" protocol. -pred Protocol1(ghost p Place, key int) { +pred Protocol1(ghost p0 Place, key int) { // 1. Receive a message. - RecvPerm(p) && + RecvPerm(p0) && let p1, m := Recv_T(p0), Recv_R(p0) in // 2. Compute MAC tag and declassify it. - DeclassifyPerm(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))) && + let tag := MAC(key, m) in + DeclassifyPerm(p1, m, tag) && let p2 := Declassify_T(p1, m, tag) in // 3. Send MAC tag over network. - SendPerm(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))) && + SendPerm(p2, tag) && let p3 := Send_T(p2, tag) in // 4. Restart. - Protocol1(Send_T(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))), key) + Protocol1(p3, key) } type state struct { @@ -81,15 +75,26 @@ type state struct { lastMsg3 int // 3rd } -pred Protocol2(ghost p Place, s state) { +pred Protocol2(ghost p0 Place, s0 state) { // Receive a message at any time. - RecvPerm(p) && Protocol2(Recv_T(p), Recv_S(s, Recv_R(p))) && + RecvPerm(p0) && + let p1, s1 := Recv_T(p0), Recv_S(s0, Recv_R(p0)) in Protocol2(p1, s1) && // NOTE: at the moment we can declassify things before receiving anything - // Declassify and send either the most or the 2nd most recently received message. - DeclassifyPerm(p, s.lastMsg1, MAC(s.key, s.lastMsg1)) && Protocol2(Declassify_T(p, s.lastMsg1, MAC(s.key, s.lastMsg1)), s) && - DeclassifyPerm(p, s.lastMsg2, MAC(s.key, s.lastMsg2)) && Protocol2(Declassify_T(p, s.lastMsg2, MAC(s.key, s.lastMsg2)), s) && - SendPerm(p, MAC(s.key, s.lastMsg1)) && Protocol2(Send_T(p, MAC(s.key, s.lastMsg1)), s) && - SendPerm(p, MAC(s.key, s.lastMsg2)) && Protocol2(Send_T(p, MAC(s.key, s.lastMsg2)), s) + // Declassify and send either the MAC tag of the most or the 2nd most + // recently received message. + let tag1, tag2 := MAC(s0.key, s0.lastMsg1), MAC(s0.key, s0.lastMsg2) in + + DeclassifyPerm(p0, s0.lastMsg1, tag1) && + let p1 := Declassify_T(p0, s0.lastMsg1, tag1) in Protocol2(p1, s0) && + + DeclassifyPerm(p0, s0.lastMsg2, tag2) && + let p1 := Declassify_T(p0, s0.lastMsg2, tag2) in Protocol2(p1, s0) && + + SendPerm(p0, tag1) && + let p1 := Send_T(p0, tag1) in Protocol2(p1, s0) && + + SendPerm(p0, tag2) && + let p1 := Send_T(p0, tag2) in Protocol2(p1, s0) } // Abstract function representing the computation of a MAC. @@ -103,30 +108,30 @@ func authenticate(ghost p0 Place, s state) { invariant token(p0) && Protocol2(p0, s) for { unfold Protocol2(p0, s) - ghost p1 := Recv_T(p0) - m1 := Recv(p0) + // ghost p1 := Recv_T(p0) + p1, m1 := Recv(p0) s = Recv_S(s, m1) unfold Protocol2(p1, s) - ghost p2 := Recv_T(p1) - m2 := Recv(p1) + // ghost p2 := Recv_T(p1) + p2, m2 := Recv(p1) s = Recv_S(s, m2) unfold Protocol2(p2, s) - ghost p3 := Recv_T(p2) - m3 := Recv(p2) + // ghost p3 := Recv_T(p2) + p3, m3 := Recv(p2) s = Recv_S(s, m3) // We can use m2, m3 here. m1 won't work. t := MAC(s.key, m3) unfold Protocol2(p3, s) - ghost p4 := Declassify_T(p3, m3, t) - Declassify(p3, m3, t) + // ghost p4 := Declassify_T(p3, m3, t) + ghost p4 := Declassify(p3, m3, t) unfold Protocol2(p4, s) - ghost p0 = Send_T(p4, t) - Send(p4, t) + // ghost p0 = Send_T(p4, t) + p0 = Send(p4, t) } } \ No newline at end of file From df0fed8f54f5204c0c2a29362356f5a40ccd8984 Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 17 Dec 2024 15:37:59 +0100 Subject: [PATCH 04/22] Fix package names and remove state.lastMsg3 --- verification/scratch/mwe1/mwe1.gobra | 2 +- verification/scratch/mwe2/mwe2.gobra | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/verification/scratch/mwe1/mwe1.gobra b/verification/scratch/mwe1/mwe1.gobra index 97d747383..7d94d32d7 100644 --- a/verification/scratch/mwe1/mwe1.gobra +++ b/verification/scratch/mwe1/mwe1.gobra @@ -3,7 +3,7 @@ // 1. We receive a message M over the network. // 2. We compute a "MAC tag" of M using K. // 3. We send the computed tag over the network. -package mwe +package mwe1 ////////////////////////////// I/O Actions ////////////////////////////// // cf. running-example/policy/actions.gobra diff --git a/verification/scratch/mwe2/mwe2.gobra b/verification/scratch/mwe2/mwe2.gobra index 477bdf79f..b2844c7f0 100644 --- a/verification/scratch/mwe2/mwe2.gobra +++ b/verification/scratch/mwe2/mwe2.gobra @@ -1,5 +1,5 @@ // Minimal working example 2. -package mwe +package mwe2 // Used to track position in protocol. type Place int @@ -21,7 +21,7 @@ pure func Recv_R(ghost p Place) int // This is how the state is/should be updated after receiving message `m`. decreases pure func Recv_S(s state, m int) state { - return state { key: s.key, lastMsg1: m, lastMsg2: s.lastMsg1, lastMsg3: s.lastMsg2 } + return state { key: s.key, lastMsg1: m, lastMsg2: s.lastMsg1 } } requires token(p) && RecvPerm(p) @@ -72,7 +72,6 @@ type state struct { key int // the private key lastMsg1 int // 1st most recently received message lastMsg2 int // 2nd - lastMsg3 int // 3rd } pred Protocol2(ghost p0 Place, s0 state) { From 76262eaeb68aaedea33cd2011cbc87e978acfc13 Mon Sep 17 00:00:00 2001 From: henriman Date: Wed, 29 Jan 2025 21:56:01 +0100 Subject: [PATCH 05/22] Lay out moving the "MAC assumption" into FullMAC This relates the abstraction of the computed MAC tag to the one computed from the abstracted arguments, s.t. we can assert `hf_valid` from there. --- pkg/slayers/path/io_msgterm_spec.gobra | 19 ++++++++++++- pkg/slayers/path/mac.go | 25 ++++++++++++++--- router/dataplane.go | 27 ++++++++++++++++++- .../crypto/subtle/constant_time.gobra | 1 + 4 files changed, 67 insertions(+), 5 deletions(-) diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra index 601db4004..0d0ca8b94 100644 --- a/pkg/slayers/path/io_msgterm_spec.gobra +++ b/pkg/slayers/path/io_msgterm_spec.gobra @@ -18,7 +18,7 @@ package path import ( "verification/io" - . "verification/utils/definitions" + . "verification/utils/definitions" ) // At the moment, we assume that all cryptographic operations performed at the code level @@ -34,6 +34,11 @@ ghost decreases pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm) +// SIF: Version for FullMAC +// ghost +// decreases +// pure func AbsFullMac(mac [MACBufferSize]byte) (io.IO_msgterm) + // The following function converts a slice with at least `MacLen` elements into // an (exclusive) array containing the mac. Note that there are no permissions // involved for accessing exclusive arrays. @@ -47,6 +52,18 @@ pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte) { return [MacLen]byte{ mac[0], mac[1], mac[2], mac[3], mac[4], mac[5] } } +// SIF: Version for FullMAC +// ghost +// requires MACBufferSize <= len(mac) +// requires forall i int :: { &mac[i] } 0 <= i && i < MACBufferSize ==> acc(&mac[i], _) +// ensures len(res) == MACBufferSize +// ensures forall i int :: { res[i] } 0 <= i && i < MACBufferSize ==> mac[i] == res[i] +// decreases +// pure func FromSliceToFullMacArray(mac []byte) (res [MACBufferSize]byte) { +// // NOTE: formatting this differently caused a parsing problem +// return [MACBufferSize]byte{ mac[0], mac[1], mac[2], mac[3], mac[4], mac[5], mac[6], mac[7], mac[8], mac[9], mac[10], mac[11], mac[12], mac[13], mac[14], mac[15] } +// } + ghost requires len(mac1) == MacLen requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index df11254b7..5d2d47557 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -21,6 +21,7 @@ import ( "hash" //@ . "github.com/scionproto/scion/verification/utils/definitions" //@ sl "github.com/scionproto/scion/verification/utils/slices" + //@ io "verification/io" ) const MACBufferSize = 16 @@ -33,8 +34,8 @@ const MACBufferSize = 16 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() // @ decreases -func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) [MacLen]byte { - mac := FullMAC(h, info, hf, buffer) +func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost dp io.DataPlaneSpec @*/) [MacLen]byte { + mac := FullMAC(h, info, hf, buffer /*@, dp @*/) var res /*@ @ @*/ [MacLen]byte //@ unfold sl.Bytes(mac, 0, MACBufferSize) copy(res[:], mac[:MacLen] /*@, R1 @*/) @@ -49,9 +50,19 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) [MacLen]byte { // @ requires h != nil && h.Mem() // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() +// // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) +// +// NOTE: We use AbsMac(FromSliceToMacArray(...)) here bc. in `verifyCurrentMac` +// we don't compare whole length. +// TODO: Can I alternatively use [:MacLen]? +// @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in +// @ let absInf := info.ToAbsInfoField() in +// @ let absHF := hf.ToIO_HF() in +// @ let absMac := AbsMac(FromSliceToMacArray(res)) in +// @ absMac == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) // @ decreases -func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) (res []byte) { +func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost dp io.DataPlaneSpec @*/) (res []byte) { if len(buffer) < MACBufferSize { buffer = make([]byte, MACBufferSize) //@ fold sl.Bytes(buffer, 0, len(buffer)) @@ -69,6 +80,14 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) (res []byt } //@ assert h.Size() >= 16 res = h.Sum(buffer[:0])[:16] + + // NOTE: This is our "MAC assumption" linking the abstraction of the + // concrete MAC tag to the abstract computation of the MAC tag. + //@ absInf := info.ToAbsInfoField() + //@ absHF := hf.ToIO_HF() + //@ absMac := AbsMac(FromSliceToMacArray(res)) + //@ AssumeForIO(absMac == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf. UInfo)) + //@ fold sl.Bytes(res, 0, MACBufferSize) return res } diff --git a/router/dataplane.go b/router/dataplane.go index 1ade5d5d7..a45a5b051 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2869,6 +2869,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput) + // NOTE: Might need FromSliceToMacArray here and maybe [:path.MacLen] on hopField.Mac + // @ ghost absMac := path.AbsMac(fullMac[:path.MacLen]) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ defer unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) @@ -2903,15 +2905,38 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ } return tmpRes, tmpErr } + + // NOTE: We want to establish hf_valid (or rather hf_valid_impl) = true here + // To that end, we need to relate abstract and concrete inif, egif, hvf, ts, uinfo etc. + // nextMsgtermSpec should be done by FullMAC + // Add the full MAC to the SCION packet processor, // such that EPIC does not need to recalculate it. p.cachedMac = fullMac // @ reveal p.EqAbsInfoField(oldPkt) // @ reveal p.EqAbsHopField(oldPkt) + + // NOTE: taken out for now // (VerifiedSCION) Assumptions for Cryptography: + // absInf := p.infoField.ToAbsInfoField() + // absHF := p.hopField.ToIO_HF() + // AssumeForIO(dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF)) + + // NOTE: This should be assert-able after `if` from postcondition of `ConstantTimeCompare`. + // @ assert hopField.Mac == fullMac[:path.MacLen] + + // @ AbsMacArrayCongruence(hopField.Mac, fullMac[:path.MacLen]) + // NOTE: ==> path.AbsMac(hopField.Mac) == path.AbsMac(fullMac[:path.MacLen]) + // @ absInf := p.infoField.ToAbsInfoField() // @ absHF := p.hopField.ToIO_HF() - // @ AssumeForIO(dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF)) + // NOTE: This should be assert-able after FullMAC(...) + // @ assert absMac == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) + // NOTE: ==> path.AbsMac(hopField.Mac) == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHf.EgIF2, absInf.AInfo, absInf.UInfo) + // NOTE: ==> absHF.HVF := path.AbsMac(hopField.Mac) == ... + // @ assert dp.hf_valid_impl(dp.Asid(), absInf.AInfo, absInf.UInfo, absHF) + // @ assert dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF) + // @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp) // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra index 8ecebd1c8..7b2d94bda 100644 --- a/verification/dependencies/crypto/subtle/constant_time.gobra +++ b/verification/dependencies/crypto/subtle/constant_time.gobra @@ -20,5 +20,6 @@ requires acc(sl.Bytes(y, 0, len(y)), _) // ensures unfolding sl.Bytes(x, 0, len(x)) in (unfolding sl.Bytes(y, 0, len(y)) in len(x) == len(y) ==> (forall i int :: 0 <= i && i < len(x) ==> x[i] == y[i]) ==> res == 1) // ensures unfolding sl.Bytes(x, 0, len(x)) in (unfolding sl.Bytes(y, 0, len(y)) in len(x) == len(y) ==> !(forall i int :: 0 <= i && i < len(x) ==> x[i] == y[i]) ==> res == 0) ensures len(x) != len(y) ==> res == 0 +ensures res != 0 ==> unfolding sl.Bytes(x, 0, len(x)) in (unfolding sl.bytes(y, 0, len(y)) in forall i int :: 0 <= i && i < len(x) ==> x[i] == y[i]) decreases _ pure func ConstantTimeCompare(x, y []byte) (res int) From 9450033dd5136a0c75d9877bb79170e89e50ab4c Mon Sep 17 00:00:00 2001 From: henriman Date: Wed, 19 Feb 2025 16:32:03 +0100 Subject: [PATCH 06/22] Remove MWEs here and implement work-around for package clauses --- pkg/slayers/doc.go | 2 +- verification/scratch/mwe1/mwe1.gobra | 265 --------------------------- verification/scratch/mwe2/mwe2.gobra | 136 -------------- 3 files changed, 1 insertion(+), 402 deletions(-) delete mode 100644 verification/scratch/mwe1/mwe1.gobra delete mode 100644 verification/scratch/mwe2/mwe2.gobra diff --git a/pkg/slayers/doc.go b/pkg/slayers/doc.go index d27e24f6e..59c9844bb 100644 --- a/pkg/slayers/doc.go +++ b/pkg/slayers/doc.go @@ -63,7 +63,7 @@ even branching based on layer type... it'll handle an (scn, e2e, udp) or (scn, h Note: Great care has been taken to only lazily parse the SCION header, however, HBH and E2E extensions are currently eagerly parsed (if they exist). Thus, handling packets containing these -extensions will be much slower (see the package benchmarks for reference). +extensions will be much slower (see the Package benchmarks for reference). When using the DecodingLayerParser, the extensions can be explicitly skipped by using the HopByHop/EndToEndExtnSkipper layer. The content of this Skipper-layer can be decoded into the full representation when necessary. diff --git a/verification/scratch/mwe1/mwe1.gobra b/verification/scratch/mwe1/mwe1.gobra deleted file mode 100644 index 7d94d32d7..000000000 --- a/verification/scratch/mwe1/mwe1.gobra +++ /dev/null @@ -1,265 +0,0 @@ -// Minimal working example 1. Only implements very basic structure. -// 0. The key K is already given. -// 1. We receive a message M over the network. -// 2. We compute a "MAC tag" of M using K. -// 3. We send the computed tag over the network. -package mwe1 - -////////////////////////////// I/O Actions ////////////////////////////// -// cf. running-example/policy/actions.gobra - -// Definition of I/O actions (abstract, for trace). -type Action adt { - RecvIO{int} - SendIO{int} - // NOTE: I have left out `p` (cf. paper) for now - // It would be necessary once we have multiple options of which message to - // declassify at some point in order to make this deterministic in the - // previous I/O actions again. However, at the moment, our IOD spec only - // allows declassifying one message depending on the previous I/O actions - DeclassifyIO{int} -} - -// Extract input of I/O action. 0 signifies no input. -ghost -decreases -pure func (a Action) Input() int { - return match a { - case RecvIO{?m}: m - case SendIO{_}: 0 - case DeclassifyIO{_}: 0 - } -} - -// Extract output of I/O action. 0 signifies no output. -ghost -decreases -pure func (a Action) Output() int { - return match a { - case RecvIO{_}: 0 - case SendIO{?t}: t - case DeclassifyIO{?t}: t - } -} - -////////////////////////////// Classification spec. ////////////////////////////// -// cf. running-example/policy/classification.gobra -// cf. running-example/classifications/basic.gobra - -type ClassificationSpec interface { - ghost - decreases - pure Classification(Action) Specification -} - -// Gives universal access to the trace. -// `pure` ensures the resulting pointer always points to the same trace. -ghost -decreases -pure func History() *Trace - -type Trace adt { - Empty{} - Snoc{Trace;Action} // Snoc: reverse cons -} - -type Specification adt { - Spec{Observation;Observation} -} - -type Observation adt { - Value{int} // NOTE: eventually might want to switch back to any - None{} - Some{Observation} - Tuple{Observation;Observation} -} - -type ObservationTrace adt { - EmptyObs{} - SnocObs{InitObs ObservationTrace;Observation} -} - -// The following is our assertion language. -ghost -decreases -pure func True() Observation { - return None{} -} - -ghost -decreases -pure func Low(v int) Observation { - return Value{v} -} - -// Given that all sensitivity preconditions have been satisfied in the trace, -// this allows us to assume that the sensitivity postconditions are satisfied. -ghost -decreases -requires sig != nil && acc(History(), 1/2) && low(Pre(sig,*History())) -ensures acc(History(), 1/2) && low(Post(sig,*History())) -func LowPost(sig ClassificationSpec) - -// NOTE: these are the low projections mentioned in the paper -ghost -decreases -pure func pre_(spec Specification) Observation { - return match spec { - case Spec{?p, _}: p - } -} -ghost -decreases -pure func post_(spec Specification) Observation { - return match spec { - case Spec{_, ?q}: q - } -} - -ghost -decreases len(trace) -requires sig != nil -pure func Pre(sig ClassificationSpec, trace Trace) ObservationTrace { - return match trace { - case Empty{}: EmptyObs{} - case Snoc{?t, ?e}: SnocObs{Pre(sig, t), pre_(sig.Classification(e))} - } -} - -ghost -decreases len(trace) -requires sig != nil -pure func Post(sig ClassificationSpec, trace Trace) ObservationTrace { - return match trace { - case Empty{}: EmptyObs{} - case Snoc{?t, ?e}: SnocObs{Post(sig, t), post_(sig.Classification(e))} - } -} - -type DefaultClassification struct {} - -ghost -decreases -pure func (DefaultClassification) Classification(a Action) Specification { - return match a { - case DeclassifyIO{?t}: Spec{True(), Low(t)} // Make `t` low. - case _: Spec{Low(a.Output()), Low(a.Input())} - } -} - -////////////////////////////// I/O spec. ////////////////////////////// -// cf. running-example/policy/iodspec.gobra - -// We express the IODSpec as a (IOD-)guarded transition system. -type IODSpec interface { - // `Guard` specifies which I/O actions may be taken, depending on the - // (content of) the action (in particular, not on the sensitivity). - ghost - decreases - pure Guard(state, Action) bool - - ghost - decreases - pure Update(state, Action) state -} - -// NOTE: We don't need IsTrace but it is not clear how to translate Reaches. -type Restriction domain { - func Reaches(IODSpec, Trace, state) bool - - axiom { - forall r IODSpec, t Trace, s state, a Action :: { Snoc{t, a}, Reaches(r, t, s) } Reaches(r, t, s) && r.Guard(s, a) ==> Reaches(r, Snoc{t, a}, r.Update(s, a)) - } -} - -// Our I/O spec. The state is the private key and the most recently received message. -type MWE1 struct {} - -type state struct { - key int - lastMsg int -} - -// We allow send, recv to happen at any point. -// Declassify can only be called on a MAC tag of the most recently received message -// generated with the private key. -ghost -decreases -pure func (MWE1) Guard(s state, a Action) bool { - return match a { - // NOTE: This makes our IOD spec well-formed, as what is allowed to be - // declassified is now deterministic in the previous I/O actions. - case DeclassifyIO{?t}: t == MAC(s.key, s.lastMsg) - case _: true - } -} - -ghost -decreases -pure func (MWE1) Update(s state, a Action) state { - return match a { - case RecvIO{?m}: state { key: s.key, lastMsg: m } - case _: s - } -} - -////////////////////////////// Trusted library I/O ////////////////////////////// -// cf. running-example/library/library.gobra - -// Receive message `m` over network. -decreases -requires acc(History()) -ensures acc(History()) && *History() == Snoc{old(*History()), RecvIO{m}} -func Recv() (m int) - -// Send tag `t` over network. -decreases -requires acc(History()) -ensures acc(History()) && *History() == Snoc{old(*History()), SendIO{t}} -func Send(t int) - -// Declassify tag `t`. -ghost -decreases -requires acc(History()) -ensures acc(History()) && *History() == Snoc{old(*History()), DeclassifyIO{t}} -func Declassify(t int) - - -////////////////////////////// Program ////////////////////////////// - -// Abstract function representing the computation of a MAC. -// key x message -> MAC tag -decreases -pure func MAC(int, int) int - -// Receives a message, authenticates it using a MAC, and sends the resulting tag. -// The state `s` contains the private key of this router, -// and the most recently received message. -// NOTE: it should suffice here to just require Reaches(...) after the program -// has terminated, bc. at the moment we definitely terminate and there is no way -// to violate the I/O spec. and "undo" this violation later on (-> safety property). -// TODO: in the future, we should probably check this after every I/O action instead? -// In the original example, I think this is done via the shared invariant. -preserves acc(History()) && acc(s) && low(Pre(DefaultClassification{}, *History())) && Reaches(MWE1{}, *History(), *s) -func authenticate(ghost s *state) { - // NOTE: forgetting the calls to either of `Declassify` and `LowPost` - // would result in a verification error *in the postcondition* (and not in - // the call to send), as here, compliance to the classification spec is - // not checked on every I/O call, but instead on the trace at the end of - // the function call. - - m := Recv() - LowPost(DefaultClassification{}) - ghost s.lastMsg = m - - t := MAC(s.key, m) - - /* ghost */ Declassify(t) - /* ghost */ LowPost(DefaultClassification{}) - Send(t) - // The following call to `LowPost` is the only one not needed (here), - // as we don't need the postcondition of the last I/O call to verify - // the remainder of the function. - /* ghost */ LowPost(DefaultClassification{}) -} \ No newline at end of file diff --git a/verification/scratch/mwe2/mwe2.gobra b/verification/scratch/mwe2/mwe2.gobra deleted file mode 100644 index b2844c7f0..000000000 --- a/verification/scratch/mwe2/mwe2.gobra +++ /dev/null @@ -1,136 +0,0 @@ -// Minimal working example 2. -package mwe2 - -// Used to track position in protocol. -type Place int -pred token(ghost p Place) - -pred RecvPerm(ghost p Place) - -// Returns the next place after calling `Recv` from `p`. -// Avoids using an existential quantifier. -ghost -decreases -pure func Recv_T(ghost p Place) Place - -// Used to refer to the received message. -ghost -decreases -pure func Recv_R(ghost p Place) int - -// This is how the state is/should be updated after receiving message `m`. -decreases -pure func Recv_S(s state, m int) state { - return state { key: s.key, lastMsg1: m, lastMsg2: s.lastMsg1 } -} - -requires token(p) && RecvPerm(p) -ensures token(next_p) && next_p == Recv_T(p) -ensures m == Recv_R(p) -ensures low(m) -func Recv(ghost p Place) (ghost next_p Place, m int) - -pred SendPerm(ghost p Place, t int) - -ghost -decreases -pure func Send_T(ghost p Place, t int) Place - -requires token(p) && SendPerm(p, t) -requires low(t) -ensures token(next_p) && next_p == Send_T(p, t) -func Send(ghost p Place, t int) (ghost next_p Place) - -pred DeclassifyPerm(ghost p Place, tag int, t int) - -ghost -decreases -pure func Declassify_T(ghost p Place, tag int, t int) Place - -ghost -requires token(p) && DeclassifyPerm(p, tag, t) -requires low(tag) -ensures token(next_p) && next_p == Declassify_T(p, tag, t) -ensures low(t) -decreases -func Declassify(ghost p Place, tag int, t int) (ghost next_p Place) - -// "Linear" protocol. -pred Protocol1(ghost p0 Place, key int) { - // 1. Receive a message. - RecvPerm(p0) && let p1, m := Recv_T(p0), Recv_R(p0) in - // 2. Compute MAC tag and declassify it. - let tag := MAC(key, m) in - DeclassifyPerm(p1, m, tag) && let p2 := Declassify_T(p1, m, tag) in - // 3. Send MAC tag over network. - SendPerm(p2, tag) && let p3 := Send_T(p2, tag) in - // 4. Restart. - Protocol1(p3, key) -} - -type state struct { - key int // the private key - lastMsg1 int // 1st most recently received message - lastMsg2 int // 2nd -} - -pred Protocol2(ghost p0 Place, s0 state) { - // Receive a message at any time. - RecvPerm(p0) && - let p1, s1 := Recv_T(p0), Recv_S(s0, Recv_R(p0)) in Protocol2(p1, s1) && - // NOTE: at the moment we can declassify things before receiving anything - // Declassify and send either the MAC tag of the most or the 2nd most - // recently received message. - let tag1, tag2 := MAC(s0.key, s0.lastMsg1), MAC(s0.key, s0.lastMsg2) in - - DeclassifyPerm(p0, s0.lastMsg1, tag1) && - let p1 := Declassify_T(p0, s0.lastMsg1, tag1) in Protocol2(p1, s0) && - - DeclassifyPerm(p0, s0.lastMsg2, tag2) && - let p1 := Declassify_T(p0, s0.lastMsg2, tag2) in Protocol2(p1, s0) && - - SendPerm(p0, tag1) && - let p1 := Send_T(p0, tag1) in Protocol2(p1, s0) && - - SendPerm(p0, tag2) && - let p1 := Send_T(p0, tag2) in Protocol2(p1, s0) -} - -// Abstract function representing the computation of a MAC. -// key x message -> MAC tag -decreases -pure func MAC(int, int) int - -requires token(p0) && Protocol2(p0, s) -func authenticate(ghost p0 Place, s state) { - - invariant token(p0) && Protocol2(p0, s) - for { - unfold Protocol2(p0, s) - // ghost p1 := Recv_T(p0) - p1, m1 := Recv(p0) - s = Recv_S(s, m1) - - unfold Protocol2(p1, s) - // ghost p2 := Recv_T(p1) - p2, m2 := Recv(p1) - s = Recv_S(s, m2) - - unfold Protocol2(p2, s) - // ghost p3 := Recv_T(p2) - p3, m3 := Recv(p2) - s = Recv_S(s, m3) - - // We can use m2, m3 here. m1 won't work. - t := MAC(s.key, m3) - - unfold Protocol2(p3, s) - // ghost p4 := Declassify_T(p3, m3, t) - ghost p4 := Declassify(p3, m3, t) - - unfold Protocol2(p4, s) - // ghost p0 = Send_T(p4, t) - p0 = Send(p4, t) - } - -} \ No newline at end of file From 418ebc40b2beb82146ab06204471ecd4f4cb9896 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 24 Feb 2025 15:42:20 +0100 Subject: [PATCH 07/22] Try reordering annotations --- pkg/slayers/path/io_msgterm_spec.gobra | 2 +- pkg/slayers/path/mac.go | 27 +++++--- router/dataplane.go | 66 ++++++++++++------- .../crypto/subtle/constant_time.gobra | 9 ++- 4 files changed, 66 insertions(+), 38 deletions(-) diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra index af3067681..05da27900 100644 --- a/pkg/slayers/path/io_msgterm_spec.gobra +++ b/pkg/slayers/path/io_msgterm_spec.gobra @@ -65,7 +65,7 @@ pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte) { // } ghost -requires len(mac1) == MacLen +requires len(mac1) >= MacLen requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50) requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> mac1[i] == mac2[i] ensures forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index 5d2d47557..c1b1ac5a4 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -34,8 +34,8 @@ const MACBufferSize = 16 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() // @ decreases -func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost dp io.DataPlaneSpec @*/) [MacLen]byte { - mac := FullMAC(h, info, hf, buffer /*@, dp @*/) +func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) [MacLen]byte { + mac := FullMAC(h, info, hf, buffer /*@, as_ @*/) var res /*@ @ @*/ [MacLen]byte //@ unfold sl.Bytes(mac, 0, MACBufferSize) copy(res[:], mac[:MacLen] /*@, R1 @*/) @@ -53,16 +53,19 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost dp i // // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // -// NOTE: We use AbsMac(FromSliceToMacArray(...)) here bc. in `verifyCurrentMac` -// we don't compare whole length. -// TODO: Can I alternatively use [:MacLen]? +// NOTE: It might make sense to use `[:MacLen]` instead of `FromSliceToMacArray`, +// as that is what is ultimately used in `verifyCurrentMAC`. // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in // @ let absInf := info.ToAbsInfoField() in // @ let absHF := hf.ToIO_HF() in // @ let absMac := AbsMac(FromSliceToMacArray(res)) in -// @ absMac == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) // @ decreases -func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost dp io.DataPlaneSpec @*/) (res []byte) { +// TODO: Test if underscore after as is really necessary +// TODO: think about if it makes sense to have as_ here. In abstraction, we need +// that information in order to get the correct key; in the concrete, the key +// is already encapsulated in hash. Maybe there is a way to relate them +func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (res []byte) { if len(buffer) < MACBufferSize { buffer = make([]byte, MACBufferSize) //@ fold sl.Bytes(buffer, 0, len(buffer)) @@ -81,12 +84,18 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost //@ assert h.Size() >= 16 res = h.Sum(buffer[:0])[:16] - // NOTE: This is our "MAC assumption" linking the abstraction of the + // NOTE: We could potentially go even further and relate + // - `io.plaintextToMac` to `MACInput` and + // - `io.mac(io.macKey(io.asidToKey(as_)), -)` to `h.Write` and `h.Sum`, + // but that might get messy. In order to verify SIF, it suffices to relate + // the result here to `io.nextMsgtermSpec`. + + // NOTE: This is our "MAC assumption", linking the abstraction of the // concrete MAC tag to the abstract computation of the MAC tag. //@ absInf := info.ToAbsInfoField() //@ absHF := hf.ToIO_HF() //@ absMac := AbsMac(FromSliceToMacArray(res)) - //@ AssumeForIO(absMac == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf. UInfo)) + //@ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf. UInfo)) //@ fold sl.Bytes(res, 0, MACBufferSize) return res diff --git a/router/dataplane.go b/router/dataplane.go index 3f7b8fd2e..807932886 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1607,7 +1607,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ unfold acc(p.d.Mem(), _) // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt)) - v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP() + v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP( /*@ dp @*/ ) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() return v1, v2 /*@, aliasesPkt, newAbsPkt @*/ @@ -2866,14 +2866,12 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ decreases func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) - fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput) - // NOTE: Might need FromSliceToMacArray here and maybe [:path.MacLen] on hopField.Mac - // @ ghost absMac := path.AbsMac(fullMac[:path.MacLen]) + fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, dp.Asid() @*/) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) - // @ defer unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) - // @ ghost defer sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) - if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { + if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen] /*@, R21 @*/) == 0 { + // ghost defer sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) + // @ defer unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ ghost ubPath := p.scionLayer.UBPath(ubScionL) // @ ghost start := p.scionLayer.PathStartIdx(ubScionL) // @ ghost end := p.scionLayer.PathEndIdx(ubScionL) @@ -2904,9 +2902,9 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, return tmpRes, tmpErr } - // NOTE: We want to establish hf_valid (or rather hf_valid_impl) = true here - // To that end, we need to relate abstract and concrete inif, egif, hvf, ts, uinfo etc. - // nextMsgtermSpec should be done by FullMAC + // sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) + // @ unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) + // @ unfold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) // Add the full MAC to the SCION packet processor, // such that EPIC does not need to recalculate it. @@ -2920,19 +2918,37 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // absHF := p.hopField.ToIO_HF() // AssumeForIO(dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF)) - // NOTE: This should be assert-able after `if` from postcondition of `ConstantTimeCompare`. - // @ assert hopField.Mac == fullMac[:path.MacLen] + // @ absHF := p.hopField.ToIO_HF() + // @ absInf := p.infoField.ToAbsInfoField() - // @ AbsMacArrayCongruence(hopField.Mac, fullMac[:path.MacLen]) - // NOTE: ==> path.AbsMac(hopField.Mac) == path.AbsMac(fullMac[:path.MacLen]) + // NOTE: After the `if`-statement, we should be able to get: + // This might need some additions to constant time compare, however + // TODO: Think about [:MacLen] vs. nothing vs. FromSliceToMacArray - // @ absInf := p.infoField.ToAbsInfoField() - // @ absHF := p.hopField.ToIO_HF() - // NOTE: This should be assert-able after FullMAC(...) - // @ assert absMac == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) - // NOTE: ==> path.AbsMac(hopField.Mac) == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHf.EgIF2, absInf.AInfo, absInf.UInfo) - // NOTE: ==> absHF.HVF := path.AbsMac(hopField.Mac) == ... - // @ assert dp.hf_valid_impl(dp.Asid(), absInf.AInfo, absInf.UInfo, absHF) + // @ assert forall i int :: { &p.hopField.Mac[:path.MacLen][i] } { fullMac[:path.MacLen][i] } 0 <= i && i < path.MacLen ==> p.hopField.Mac[:path.MacLen][i] == fullMac[:path.MacLen][i] + + // @ assert forall i int :: { &fullMac[i] } 0 <= i && i < path.MacLen ==> fullMac[i] == p.hopField.Mac[i] + + // @ path.EqualBytesImplyEqualMac(fullMac, p.hopField.Mac) + // @ assert path.AbsMac(p.hopField.Mac) == path.AbsMac(path.FromSliceToMacArray(fullMac)) + + // NOTE: We know: + // absHF.HVF := path.AbsMac(p.hopField.Mac) + + // ==> absHF.HVF := path.AbsMac(p.hopField.Mac) + // NOTE: by `AbsMacArrayCongruence` or `EqualBytesImplyEqualMac` + // == path.AbsMac(FromSliceToMacArray(fullMac)) + // == io.nextMsgtermSpec(...) + + // NOTE: From the postcondition of `FullMAC` we get: + // @ fold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) + // @ sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) + // @ unfold acc(sl.Bytes(fullMac, 0, len(fullMac)), R21) + // @ assert path.AbsMac(path.FromSliceToMacArray(fullMac)) == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) + + // NOTE: ==> + // @ assert absHF.HVF == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) + // @ assert io.hf_valid_impl(dp.Asid(), absInf.AInfo, absInf.UInfo, absHF) // @ assert dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF) // @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp) @@ -4090,7 +4106,7 @@ func (p *scionPacketProcessor) process( // @ newAbsPkt == absIO_val(respr.OutPkt, respr.EgressID) && // @ newAbsPkt.isIO_val_Unsupported // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { +func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { // @ ghost ubScionL := p.rawPkt // @ p.scionLayer.ExtractAcc(ubScionL) s := p.scionLayer @@ -4152,12 +4168,12 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error / // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases // @ outline ( - mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput) + mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput /*@, dp.Asid() @*/) // (VerifiedSCION) introduced separate copy to avoid exposing quantified permissions outside the scope of this outline block. macCopy := mac // @ fold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56) // @ fold acc(sl.Bytes(mac[:], 0, len(mac)), R56) - compRes := subtle.ConstantTimeCompare(ohp.FirstHop.Mac[:], mac[:]) == 0 + compRes := subtle.ConstantTimeCompare(ohp.FirstHop.Mac[:], mac[:] /*@, R56 @*/) == 0 // @ unfold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56) // @ ) if compRes { @@ -4229,7 +4245,7 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error / // XXX(roosd): Here we leak the buffer into the SCION packet header. // This is okay because we do not operate on the buffer or the packet // for the rest of processing. - ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput) + ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput /*@, dp.Asid() @*/) // @ fold ohp.SecondHop.Mem() // @ fold s.Path.Mem(ubPath) // @ fold acc(p.scionLayer.Mem(ubScionL), 1-R15) diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra index 68b411b07..512cd7e22 100644 --- a/verification/dependencies/crypto/subtle/constant_time.gobra +++ b/verification/dependencies/crypto/subtle/constant_time.gobra @@ -15,8 +15,11 @@ import sl "github.com/scionproto/scion/verification/utils/slices" // and 0 otherwise. The time taken is a function of the length of the slices and // is independent of the contents. trusted -requires sl.Bytes(x, 0, len(x)) -requires sl.Bytes(y, 0, len(y)) +requires p > 0 +preserves acc(sl.Bytes(x, 0, len(x)), p) +preserves acc(sl.Bytes(y, 0, len(y)), p) ensures len(x) != len(y) ==> res == 0 +// TODO: maybe package this in sl.Bytes again +ensures res != 0 ==> unfolding acc(sl.Bytes(x, 0, len(x)), p) in unfolding acc(sl.Bytes(y, 0, len(y)), p) in forall i int :: { x[i] } { y[i] } 0 <= i && i < len(x) ==> x[i] == y[i] decreases -pure func ConstantTimeCompare(x, y []byte) (res int) +func ConstantTimeCompare(x, y []byte, ghost p perm) (res int) From f35325fabcb5f8bfacd198dce2a4ecb35105b655 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 24 Feb 2025 20:02:56 +0100 Subject: [PATCH 08/22] Finish verification and clean up --- pkg/slayers/doc.go | 2 +- pkg/slayers/path/io_msgterm_spec.gobra | 17 -------- pkg/slayers/path/mac.go | 28 ++++-------- router/dataplane.go | 43 +++---------------- .../crypto/subtle/constant_time.gobra | 13 +++--- 5 files changed, 22 insertions(+), 81 deletions(-) diff --git a/pkg/slayers/doc.go b/pkg/slayers/doc.go index 59c9844bb..d27e24f6e 100644 --- a/pkg/slayers/doc.go +++ b/pkg/slayers/doc.go @@ -63,7 +63,7 @@ even branching based on layer type... it'll handle an (scn, e2e, udp) or (scn, h Note: Great care has been taken to only lazily parse the SCION header, however, HBH and E2E extensions are currently eagerly parsed (if they exist). Thus, handling packets containing these -extensions will be much slower (see the Package benchmarks for reference). +extensions will be much slower (see the package benchmarks for reference). When using the DecodingLayerParser, the extensions can be explicitly skipped by using the HopByHop/EndToEndExtnSkipper layer. The content of this Skipper-layer can be decoded into the full representation when necessary. diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra index 05da27900..918700324 100644 --- a/pkg/slayers/path/io_msgterm_spec.gobra +++ b/pkg/slayers/path/io_msgterm_spec.gobra @@ -34,11 +34,6 @@ ghost decreases pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm) -// SIF: Version for FullMAC -// ghost -// decreases -// pure func AbsFullMac(mac [MACBufferSize]byte) (io.IO_msgterm) - // The following function converts a slice with at least `MacLen` elements into // an (exclusive) array containing the mac. Note that there are no permissions // involved for accessing exclusive arrays. @@ -52,18 +47,6 @@ pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte) { return [MacLen]byte{ mac[0], mac[1], mac[2], mac[3], mac[4], mac[5] } } -// SIF: Version for FullMAC -// ghost -// requires MACBufferSize <= len(mac) -// requires forall i int :: { &mac[i] } 0 <= i && i < MACBufferSize ==> acc(&mac[i], _) -// ensures len(res) == MACBufferSize -// ensures forall i int :: { res[i] } 0 <= i && i < MACBufferSize ==> mac[i] == res[i] -// decreases -// pure func FromSliceToFullMacArray(mac []byte) (res [MACBufferSize]byte) { -// // NOTE: formatting this differently caused a parsing problem -// return [MACBufferSize]byte{ mac[0], mac[1], mac[2], mac[3], mac[4], mac[5], mac[6], mac[7], mac[8], mac[9], mac[10], mac[11], mac[12], mac[13], mac[14], mac[15] } -// } - ghost requires len(mac1) >= MacLen requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index c1b1ac5a4..a280d7291 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -53,18 +53,12 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ // // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // -// NOTE: It might make sense to use `[:MacLen]` instead of `FromSliceToMacArray`, -// as that is what is ultimately used in `verifyCurrentMAC`. -// @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in -// @ let absInf := info.ToAbsInfoField() in -// @ let absHF := hf.ToIO_HF() in -// @ let absMac := AbsMac(FromSliceToMacArray(res)) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) +// @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in +// @ let absInf := info.ToAbsInfoField() in +// @ let absHF := hf.ToIO_HF() in +// @ let absMac := AbsMac(FromSliceToMacArray(res)) in +// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases -// TODO: Test if underscore after as is really necessary -// TODO: think about if it makes sense to have as_ here. In abstraction, we need -// that information in order to get the correct key; in the concrete, the key -// is already encapsulated in hash. Maybe there is a way to relate them func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (res []byte) { if len(buffer) < MACBufferSize { buffer = make([]byte, MACBufferSize) @@ -84,18 +78,12 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost //@ assert h.Size() >= 16 res = h.Sum(buffer[:0])[:16] - // NOTE: We could potentially go even further and relate - // - `io.plaintextToMac` to `MACInput` and - // - `io.mac(io.macKey(io.asidToKey(as_)), -)` to `h.Write` and `h.Sum`, - // but that might get messy. In order to verify SIF, it suffices to relate - // the result here to `io.nextMsgtermSpec`. - - // NOTE: This is our "MAC assumption", linking the abstraction of the - // concrete MAC tag to the abstract computation of the MAC tag. + // This is our "MAC assumption", linking the abstraction of the concrete + // MAC tag to the abstract computation of the MAC tag. //@ absInf := info.ToAbsInfoField() //@ absHF := hf.ToIO_HF() //@ absMac := AbsMac(FromSliceToMacArray(res)) - //@ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf. UInfo)) + //@ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo)) //@ fold sl.Bytes(res, 0, MACBufferSize) return res diff --git a/router/dataplane.go b/router/dataplane.go index 54cd1251e..61b552b73 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2869,8 +2869,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, dp.Asid() @*/) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) - if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen] /*@, R21 @*/) == 0 { - // ghost defer sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) + if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { // @ defer unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ ghost ubPath := p.scionLayer.UBPath(ubScionL) // @ ghost start := p.scionLayer.PathStartIdx(ubScionL) @@ -2902,54 +2901,24 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, return tmpRes, tmpErr } - // sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) - // @ unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) - // @ unfold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) - // Add the full MAC to the SCION packet processor, // such that EPIC does not need to recalculate it. p.cachedMac = fullMac // @ reveal p.EqAbsInfoField(oldPkt) // @ reveal p.EqAbsHopField(oldPkt) - // NOTE: taken out for now - // (VerifiedSCION) Assumptions for Cryptography: - // absInf := p.infoField.ToAbsInfoField() - // absHF := p.hopField.ToIO_HF() - // AssumeForIO(dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF)) - // @ absHF := p.hopField.ToIO_HF() // @ absInf := p.infoField.ToAbsInfoField() - // NOTE: After the `if`-statement, we should be able to get: - // This might need some additions to constant time compare, however - // TODO: Think about [:MacLen] vs. nothing vs. FromSliceToMacArray - - // @ assert forall i int :: { &p.hopField.Mac[:path.MacLen][i] } { fullMac[:path.MacLen][i] } 0 <= i && i < path.MacLen ==> p.hopField.Mac[:path.MacLen][i] == fullMac[:path.MacLen][i] - - // @ assert forall i int :: { &fullMac[i] } 0 <= i && i < path.MacLen ==> fullMac[i] == p.hopField.Mac[i] - + // @ unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) + // @ unfold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) // @ path.EqualBytesImplyEqualMac(fullMac, p.hopField.Mac) - // @ assert path.AbsMac(p.hopField.Mac) == path.AbsMac(path.FromSliceToMacArray(fullMac)) - - // NOTE: We know: - // absHF.HVF := path.AbsMac(p.hopField.Mac) - // ==> absHF.HVF := path.AbsMac(p.hopField.Mac) - // NOTE: by `AbsMacArrayCongruence` or `EqualBytesImplyEqualMac` // == path.AbsMac(FromSliceToMacArray(fullMac)) - // == io.nextMsgtermSpec(...) - // NOTE: From the postcondition of `FullMAC` we get: - // @ fold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) - // @ sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21) + // Needed to "access" postcondition of `FullMAC`: // @ unfold acc(sl.Bytes(fullMac, 0, len(fullMac)), R21) - // @ assert path.AbsMac(path.FromSliceToMacArray(fullMac)) == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo) - - // NOTE: ==> - // @ assert absHF.HVF == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) - // @ assert io.hf_valid_impl(dp.Asid(), absInf.AInfo.V, absInf.UInfo, absHF) - // @ assert dp.hf_valid(absInf.ConsDir, absInf.AInfo.V, absInf.UInfo, absHF) + // ==> absHF.HVF == io.nextMsgtermSpec(...) // @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp) // @ fold p.d.validResult(processResult{}, false) @@ -4173,7 +4142,7 @@ func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) ( macCopy := mac // @ fold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56) // @ fold acc(sl.Bytes(mac[:], 0, len(mac)), R56) - compRes := subtle.ConstantTimeCompare(ohp.FirstHop.Mac[:], mac[:] /*@, R56 @*/) == 0 + compRes := subtle.ConstantTimeCompare(ohp.FirstHop.Mac[:], mac[:]) == 0 // @ unfold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56) // @ ) if compRes { diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra index 512cd7e22..0e4792890 100644 --- a/verification/dependencies/crypto/subtle/constant_time.gobra +++ b/verification/dependencies/crypto/subtle/constant_time.gobra @@ -15,11 +15,12 @@ import sl "github.com/scionproto/scion/verification/utils/slices" // and 0 otherwise. The time taken is a function of the length of the slices and // is independent of the contents. trusted -requires p > 0 -preserves acc(sl.Bytes(x, 0, len(x)), p) -preserves acc(sl.Bytes(y, 0, len(y)), p) +requires sl.Bytes(x, 0, len(x)) +requires sl.Bytes(y, 0, len(y)) ensures len(x) != len(y) ==> res == 0 -// TODO: maybe package this in sl.Bytes again -ensures res != 0 ==> unfolding acc(sl.Bytes(x, 0, len(x)), p) in unfolding acc(sl.Bytes(y, 0, len(y)), p) in forall i int :: { x[i] } { y[i] } 0 <= i && i < len(x) ==> x[i] == y[i] +ensures res != 0 ==> + unfolding sl.Bytes(x, 0, len(x)) in + unfolding sl.Bytes(y, 0, len(y)) in + forall i int :: { x[i] } { y[i] } 0 <= i && i < len(x) ==> x[i] == y[i] decreases -func ConstantTimeCompare(x, y []byte, ghost p perm) (res int) +pure func ConstantTimeCompare(x, y []byte) (res int) From f6752dab061f730a36f21b70ae7304d745980e99 Mon Sep 17 00:00:00 2001 From: henriman Date: Thu, 6 Mar 2025 00:37:28 +0100 Subject: [PATCH 09/22] Start including MAC --- pkg/slayers/path/mac.go | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index a280d7291..e1f509c66 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -33,12 +33,21 @@ const MACBufferSize = 16 // @ requires h != nil && h.Mem() // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() +// @ ensures let absInf := info.ToAbsInfoField() in +// @ let absHF := hf.ToIO_HF() in +// @ let absMac := AbsMac(ret) in +// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases -func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) [MacLen]byte { +func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (ret [MacLen]byte) { mac := FullMAC(h, info, hf, buffer /*@, as_ @*/) var res /*@ @ @*/ [MacLen]byte - //@ unfold sl.Bytes(mac, 0, MACBufferSize) + // @ unfold sl.Bytes(mac, 0, MACBufferSize) + copy(res[:], mac[:MacLen] /*@, R1 @*/) + + // @ assert forall i int :: { res[i] } 0 <= i && i < len(res[:]) ==> &res[:][i] == &res[i] + // @ EqualBytesImplyEqualMac(mac, res) + return res } @@ -83,7 +92,7 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost //@ absInf := info.ToAbsInfoField() //@ absHF := hf.ToIO_HF() //@ absMac := AbsMac(FromSliceToMacArray(res)) - //@ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo, absInf.UInfo)) + //@ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) //@ fold sl.Bytes(res, 0, MACBufferSize) return res From f9aff847d31bec02038e374954b7a984a22f9940 Mon Sep 17 00:00:00 2001 From: henriman Date: Sat, 8 Mar 2025 20:02:53 +0100 Subject: [PATCH 10/22] Address PR I also adjusted the code to match the "new style conventions" (e.g. space between // and @) --- pkg/slayers/path/io_msgterm_spec.gobra | 2 +- pkg/slayers/path/mac.go | 45 +++++++++---------- router/dataplane.go | 8 ++-- .../crypto/subtle/constant_time.gobra | 7 ++- 4 files changed, 30 insertions(+), 32 deletions(-) diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra index 918700324..5976f6c12 100644 --- a/pkg/slayers/path/io_msgterm_spec.gobra +++ b/pkg/slayers/path/io_msgterm_spec.gobra @@ -18,7 +18,7 @@ package path import ( "verification/io" - . "verification/utils/definitions" + . "verification/utils/definitions" ) // At the moment, we assume that all cryptographic operations performed at the code level diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index e1f509c66..2c98df061 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -19,9 +19,9 @@ package path import ( "encoding/binary" "hash" - //@ . "github.com/scionproto/scion/verification/utils/definitions" - //@ sl "github.com/scionproto/scion/verification/utils/slices" - //@ io "verification/io" + // @ . "github.com/scionproto/scion/verification/utils/definitions" + // @ sl "github.com/scionproto/scion/verification/utils/slices" + // @ io "verification/io" ) const MACBufferSize = 16 @@ -36,16 +36,16 @@ const MACBufferSize = 16 // @ ensures let absInf := info.ToAbsInfoField() in // @ let absHF := hf.ToIO_HF() in // @ let absMac := AbsMac(ret) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (ret [MacLen]byte) { mac := FullMAC(h, info, hf, buffer /*@, as_ @*/) - var res /*@ @ @*/ [MacLen]byte + var res /*@@@*/ [MacLen]byte // @ unfold sl.Bytes(mac, 0, MACBufferSize) copy(res[:], mac[:MacLen] /*@, R1 @*/) - - // @ assert forall i int :: { res[i] } 0 <= i && i < len(res[:]) ==> &res[:][i] == &res[i] + + // @ assert forall i int :: { res[i] } 0 <= i && i < len(res[:]) ==> &res[:][i] == &res[i] // @ EqualBytesImplyEqualMac(mac, res) return res @@ -59,42 +59,41 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ // @ requires h != nil && h.Mem() // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() -// // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) -// // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in -// @ let absInf := info.ToAbsInfoField() in -// @ let absHF := hf.ToIO_HF() in +// @ let absInf := info.ToAbsInfoField() in +// @ let absHF := hf.ToIO_HF() in // @ let absMac := AbsMac(FromSliceToMacArray(res)) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (res []byte) { if len(buffer) < MACBufferSize { buffer = make([]byte, MACBufferSize) - //@ fold sl.Bytes(buffer, 0, len(buffer)) + // @ fold sl.Bytes(buffer, 0, len(buffer)) } h.Reset() MACInput(info.SegID, info.Timestamp, hf.ExpTime, hf.ConsIngress, hf.ConsEgress, buffer) - //@ unfold sl.Bytes(buffer, 0, len(buffer)) - //@ defer fold sl.Bytes(buffer, 0, len(buffer)) + // @ unfold sl.Bytes(buffer, 0, len(buffer)) + // @ defer fold sl.Bytes(buffer, 0, len(buffer)) // Write must not return an error: https://godoc.org/hash#Hash if _, err := h.Write(buffer); err != nil { // @ Unreachable() panic(err) } - //@ assert h.Size() >= 16 + // @ assert h.Size() >= 16 res = h.Sum(buffer[:0])[:16] - // This is our "MAC assumption", linking the abstraction of the concrete - // MAC tag to the abstract computation of the MAC tag. - //@ absInf := info.ToAbsInfoField() - //@ absHF := hf.ToIO_HF() - //@ absMac := AbsMac(FromSliceToMacArray(res)) - //@ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) + // @ absInf := info.ToAbsInfoField() + // @ absHF := hf.ToIO_HF() + // @ absMac := AbsMac(FromSliceToMacArray(res)) + + // This is our "MAC assumption", linking the abstraction of the concrete MAC + // tag to the abstract computation of the MAC tag. + // @ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) - //@ fold sl.Bytes(res, 0, MACBufferSize) + // @ fold sl.Bytes(res, 0, MACBufferSize) return res } diff --git a/router/dataplane.go b/router/dataplane.go index 61b552b73..c5849b002 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2910,15 +2910,15 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ absHF := p.hopField.ToIO_HF() // @ absInf := p.infoField.ToAbsInfoField() + // @ assert forall i int :: { sl.GetByte(fullMac[:path.MacLen], 0, path.MacLen, i) } 0 <= i && i < path.MacLen ==> + // @ sl.GetByte(fullMac[:path.MacLen], 0, path.MacLen, i) == + // @ unfolding acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) in fullMac[i] // @ unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ unfold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) // @ path.EqualBytesImplyEqualMac(fullMac, p.hopField.Mac) - // ==> absHF.HVF := path.AbsMac(p.hopField.Mac) - // == path.AbsMac(FromSliceToMacArray(fullMac)) - // Needed to "access" postcondition of `FullMAC`: // @ unfold acc(sl.Bytes(fullMac, 0, len(fullMac)), R21) - // ==> absHF.HVF == io.nextMsgtermSpec(...) + // @ assert absHF.HVF == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp) // @ fold p.d.validResult(processResult{}, false) diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra index 0e4792890..8635d9a78 100644 --- a/verification/dependencies/crypto/subtle/constant_time.gobra +++ b/verification/dependencies/crypto/subtle/constant_time.gobra @@ -18,9 +18,8 @@ trusted requires sl.Bytes(x, 0, len(x)) requires sl.Bytes(y, 0, len(y)) ensures len(x) != len(y) ==> res == 0 -ensures res != 0 ==> - unfolding sl.Bytes(x, 0, len(x)) in - unfolding sl.Bytes(y, 0, len(y)) in - forall i int :: { x[i] } { y[i] } 0 <= i && i < len(x) ==> x[i] == y[i] +ensures res != 0 ==> + forall i int :: { sl.GetByte(x, 0, len(x), i) }{ sl.GetByte(y, 0, len(y), i) } 0 <= i && i < len(x) ==> + sl.GetByte(x, 0, len(x), i) == sl.GetByte(y, 0, len(y), i) decreases pure func ConstantTimeCompare(x, y []byte) (res int) From aa51dda6e6c3f27f56f455bf78b25daa7394c4a4 Mon Sep 17 00:00:00 2001 From: henriman Date: Wed, 2 Apr 2025 21:45:57 +0200 Subject: [PATCH 11/22] Start adding AS identifer to hash --- pkg/scrypto/scrypto_spec.gobra | 16 +++++-- pkg/slayers/doc.go | 2 +- pkg/slayers/path/mac.go | 20 ++++---- pkg/slayers/scion_spec.gobra | 20 ++++---- router/dataplane.go | 57 ++++++++++++++++++----- router/dataplane_spec.gobra | 15 ++++-- router/dataplane_spec_test.gobra | 3 +- verification/dependencies/hash/hash.gobra | 22 ++++++++- 8 files changed, 111 insertions(+), 44 deletions(-) diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra index b33787ac5..12d80b36a 100644 --- a/pkg/scrypto/scrypto_spec.gobra +++ b/pkg/scrypto/scrypto_spec.gobra @@ -19,8 +19,11 @@ package scrypto -import "hash" -import sl "github.com/scionproto/scion/verification/utils/slices" +import ( + "hash" + sl "github.com/scionproto/scion/verification/utils/slices" + "github.com/scionproto/scion/verification/io" +) // The error returned by initMac is produced deterministically depending on the key. // If an initial call to initmac succeeds with a key, then any subsequent @@ -33,7 +36,12 @@ pure func ValidKeyForHash(key []byte) bool preserves acc(sl.Bytes(key, 0, len(key)), _) ensures old(ValidKeyForHash(key)) ==> e == nil -ensures e == nil ==> (h != nil && h.Mem() && ValidKeyForHash(key)) +ensures e == nil ==> ( + h != nil && + h.Mem() && + ValidKeyForHash(key) && + h === sh && + sh.Asid() == asid) ensures e != nil ==> e.ErrorMem() decreases _ -func InitMac(key []byte) (h hash.Hash, e error) +func InitMac(key []byte, ghost asid io.IO_as) (h hash.Hash, ghost sh hash.ScionHashSpec, e error) diff --git a/pkg/slayers/doc.go b/pkg/slayers/doc.go index d27e24f6e..59c9844bb 100644 --- a/pkg/slayers/doc.go +++ b/pkg/slayers/doc.go @@ -63,7 +63,7 @@ even branching based on layer type... it'll handle an (scn, e2e, udp) or (scn, h Note: Great care has been taken to only lazily parse the SCION header, however, HBH and E2E extensions are currently eagerly parsed (if they exist). Thus, handling packets containing these -extensions will be much slower (see the package benchmarks for reference). +extensions will be much slower (see the Package benchmarks for reference). When using the DecodingLayerParser, the extensions can be explicitly skipped by using the HopByHop/EndToEndExtnSkipper layer. The content of this Skipper-layer can be decoded into the full representation when necessary. diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index 2c98df061..27e7025e8 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -30,16 +30,16 @@ const MACBufferSize = 16 // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. -// @ requires h != nil && h.Mem() +// @ requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() +// @ ensures h.Mem() && sh === h // @ ensures let absInf := info.ToAbsInfoField() in // @ let absHF := hf.ToIO_HF() in // @ let absMac := AbsMac(ret) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases -func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (ret [MacLen]byte) { - mac := FullMAC(h, info, hf, buffer /*@, as_ @*/) +func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh hash.ScionHashSpec @*/) (ret [MacLen]byte) { + mac := FullMAC(h, info, hf, buffer /*@, sh @*/) var res /*@@@*/ [MacLen]byte // @ unfold sl.Bytes(mac, 0, MACBufferSize) @@ -56,17 +56,17 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. // In contrast to MAC(), FullMAC returns all the 16 bytes instead of only 6 bytes of the MAC. -// @ requires h != nil && h.Mem() +// @ requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() +// @ ensures h.Mem() && sh === h // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in // @ let absInf := info.ToAbsInfoField() in // @ let absHF := hf.ToIO_HF() in // @ let absMac := AbsMac(FromSliceToMacArray(res)) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases -func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (res []byte) { +func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh hash.ScionHashSpec @*/) (res []byte) { if len(buffer) < MACBufferSize { buffer = make([]byte, MACBufferSize) // @ fold sl.Bytes(buffer, 0, len(buffer)) @@ -91,7 +91,7 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost // This is our "MAC assumption", linking the abstraction of the concrete MAC // tag to the abstract computation of the MAC tag. - // @ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) + // @ AssumeForIO(absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) // @ fold sl.Bytes(res, 0, MACBufferSize) return res diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 3f92aff1e..e45ae6064 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -409,20 +409,20 @@ requires sl.Bytes(ub, 0, len(ub)) decreases pure func (s *SCION) EqAbsHeader(ub []byte) bool { return unfolding s.Mem(ub) in - let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in + let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in let high := s.HdrLen*LineLen in - GetAddressOffset(ub) == low && + GetAddressOffset(ub) == low_ && GetLength(ub) == int(high) && // Might be worth introducing EqAbsHeader as an interface method on Path // to avoid doing these casts, especially when we add support for EPIC. typeOf(s.Path) == (*scion.Raw) && - unfolding s.Path.Mem(ub[low:high]) in + unfolding s.Path.Mem(ub[low_:high]) in unfolding sl.Bytes(ub, 0, len(ub)) in - let _ := Asserting(forall k int :: {&ub[low:high][k]} 0 <= k && k < high ==> - &ub[low:high][k] == &ub[low + k]) in - let _ := Asserting(forall k int :: {&ub[low:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> - &ub[low:high][:scion.MetaLen][k] == &ub[low:high][k]) in - let metaHdr := scion.DecodedFrom(binary.BigEndian.Uint32(ub[low:high][:scion.MetaLen])) in + let _ := Asserting(forall k int :: {&ub[low_:high][k]} 0 <= k && k < high ==> + &ub[low_:high][k] == &ub[low_ + k]) in + let _ := Asserting(forall k int :: {&ub[low_:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> + &ub[low_:high][:scion.MetaLen][k] == &ub[low_:high][k]) in + let metaHdr := scion.DecodedFrom(binary.BigEndian.Uint32(ub[low_:high][:scion.MetaLen])) in let seg1 := int(metaHdr.SegLen[0]) in let seg2 := int(metaHdr.SegLen[1]) in let seg3 := int(metaHdr.SegLen[2]) in @@ -438,10 +438,10 @@ requires s.Mem(ub) decreases pure func (s *SCION) ValidScionInitSpec(ub []byte) bool { return unfolding s.Mem(ub) in - let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in + let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in let high := s.HdrLen*LineLen in typeOf(s.Path) == (*scion.Raw) && - s.Path.(*scion.Raw).GetBase(ub[low:high]).WeaklyValid() + s.Path.(*scion.Raw).GetBase(ub[low_:high]).WeaklyValid() } // Checks if the common path header is valid in the serialized scion packet. diff --git a/router/dataplane.go b/router/dataplane.go index c5849b002..224ef336a 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -187,6 +187,9 @@ type DataPlane struct { // (VerifiedSCION) This is stored in the dataplane in order to retain // knowledge that macFactory will not fail. // @ ghost key *[]byte + // TODO: See if there is a way to circumvent storing `asid`, considering + // that this can be generated from `localIA`. + // @ ghost asid gpointer[io.IO_as] external map[uint16]BatchConn linkTypes map[uint16]topology.LinkType neighborIAs map[uint16]addr.IA @@ -194,7 +197,7 @@ type DataPlane struct { internalIP net.IP internalNextHops map[uint16]*net.UDPAddr svc *services - macFactory func() hash.Hash + macFactory func() (hash.Hash /*@, ghost hash.ScionHashSpec @*/) bfdSessions map[uint16]bfdSession localIA addr.IA mtx sync.Mutex @@ -311,22 +314,28 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // @ Unreachable() return alreadySet } + + // @ ghost asid@ := io.IO_as{uint(d.localIA)} + // First check for MAC creation errors. - if _, err := scrypto.InitMac(key); err != nil { + if _ /*@, macSpec @*/, err := scrypto.InitMac(key /*@, asid @*/); err != nil { return err } // @ d.key = &key + // @ d.asid = &asid verScionTemp := // @ requires acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _) // @ requires scrypto.ValidKeyForHash(key) + // @ requires acc(&asid, _) // @ ensures acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _) // @ ensures h != nil && h.Mem() + // @ ensures acc(&asid, _) && sh === h && sh.Asid() == asid // @ decreases - func /*@ f @*/ () (h hash.Hash) { - mac, _ := scrypto.InitMac(key) - return mac + func /*@ f @*/ () (h hash.Hash /*@, ghost sh hash.ScionHashSpec @*/) { + mac /*@, macSpec @*/, _ := scrypto.InitMac(key /*@, asid @*/) + return mac /*@, macSpec @*/ } - // @ proof verScionTemp implements MacFactorySpec{d.key} { + // @ proof verScionTemp implements MacFactorySpec{d.key, d.asid} { // @ return verScionTemp() as f // @ } d.macFactory = verScionTemp @@ -515,6 +524,7 @@ func (d *DataPlane) AddExternalInterfaceBFD(ifID uint16, conn BatchConn, PacketsReceived: d.Metrics.BFDPacketsReceived.With(labels), } } + // TODO: Now that macFactory returns two arguments, might want to move this out? s := newBFDSend(conn, src.IA, dst.IA, src.Addr, dst.Addr, ifID, d.macFactory()) return d.addBFDController(ifID, s, cfg, m) } @@ -734,6 +744,7 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro } } + // TODO: Now that macFactory returns two values, might want to move this call out? s := newBFDSend(d.internal, d.localIA, d.localIA, src, dst, 0, d.macFactory()) return d.addBFDController(ifID, s, cfg, m) } @@ -1407,16 +1418,20 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess // @ d.getNewPacketProcessorFootprint() verScionTmp = gopacket.NewSerializeBuffer() // @ sl.PermsImplyIneqWithWildcard(verScionTmp.UBuf(), *d.key) + mac /*@, macSpec @*/ := (d.macFactory() /*@ as MacFactorySpec{d.key, d.asid} @*/) p := &scionPacketProcessor{ d: d, ingressID: ingressID, buffer: verScionTmp, - mac: (d.macFactory() /*@ as MacFactorySpec{d.key} @ */), + mac: mac, macBuffers: macBuffersT{ scionInput: make([]byte, path.MACBufferSize), epicInput: make([]byte, libepic.MACBufferSize), }, } + // TODO: Doing this "right in initialization" makes Gobra think `p` is a + // `gpointer` and not "normal pointer". + // @ p.macSpec = macSpec // @ fold sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw) p.scionLayer.RecyclePaths() @@ -1607,7 +1622,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ unfold acc(p.d.Mem(), _) // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt)) - v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP( /*@ dp @*/ ) + v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP(/*@ dp @*/) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() return v1, v2 /*@, aliasesPkt, newAbsPkt @*/ @@ -1889,6 +1904,9 @@ type scionPacketProcessor struct { buffer gopacket.SerializeBuffer // mac is the hasher for the MAC computation. mac hash.Hash + // `macSpec` let's us access the AS identifier corresponding to the private key + // used by `mac`. + // @ ghost macSpec hash.ScionHashSpec // scionLayer is the SCION gopacket layer. scionLayer slayers.SCION @@ -2826,6 +2844,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) // @ preserves acc(&p.mac, R20) && p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2866,7 +2885,9 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ decreases func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) - fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, dp.Asid() @*/) + fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/) + // TODO: Remove assertion + // @ assert p.macSpec.Asid() == dp.Asid() // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { @@ -2898,8 +2919,12 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ ghost if tmpErr != nil && tmpRes.OutPkt != nil { // @ AbsUnsupportedPktIsUnsupportedVal(tmpRes.OutPkt, tmpRes.EgressID) // @ } + // TODO: Remove assertion + // @ assert p.macSpec.Asid() == dp.Asid() return tmpRes, tmpErr } + // TODO: Remove assertion + // @ assert p.macSpec.Asid() == dp.Asid() // Add the full MAC to the SCION packet processor, // such that EPIC does not need to recalculate it. @@ -2920,6 +2945,9 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ unfold acc(sl.Bytes(fullMac, 0, len(fullMac)), R21) // @ assert absHF.HVF == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) + // TODO: Remove assertion + // @ assert p.macSpec.Asid() == dp.Asid() + // @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp) // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil @@ -3806,6 +3834,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -4050,6 +4079,7 @@ func (p *scionPacketProcessor) process( // @ requires sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ preserves acc(&p.mac, R10) // @ preserves p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() @@ -4070,12 +4100,14 @@ func (p *scionPacketProcessor) process( // contracts for IO-spec // @ requires p.scionLayer.EqPathType(p.rawPkt) // @ requires !slayers.IsSupportedPkt(p.rawPkt) +// @ requires p.d.DpAgreesWithSpec(dp) +// TODO: Might also want to require dp.Valid() // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{}) // @ ensures respr.OutPkt != nil ==> // @ newAbsPkt == absIO_val(respr.OutPkt, respr.EgressID) && // @ newAbsPkt.isIO_val_Unsupported // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { +func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { // @ ghost ubScionL := p.rawPkt // @ p.scionLayer.ExtractAcc(ubScionL) s := p.scionLayer @@ -4134,10 +4166,11 @@ func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) ( // @ preserves acc(&ohp.Info, R55) && acc(&ohp.FirstHop, R55) // @ preserves acc(&p.macBuffers.scionInput, R55) // @ preserves acc(&p.mac, R55) && p.mac != nil && p.mac.Mem() + // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases // @ outline ( - mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput /*@, dp.Asid() @*/) + mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput /*@, p.macSpec @*/) // (VerifiedSCION) introduced separate copy to avoid exposing quantified permissions outside the scope of this outline block. macCopy := mac // @ fold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56) @@ -4214,7 +4247,7 @@ func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) ( // XXX(roosd): Here we leak the buffer into the SCION packet header. // This is okay because we do not operate on the buffer or the packet // for the rest of processing. - ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput /*@, dp.Asid() @*/) + ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput /*@, p.macSpec @*/) // @ fold ohp.SecondHop.Mem() // @ fold s.Path.Mem(ubPath) // @ fold acc(p.scionLayer.Mem(ubScionL), 1-R15) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index e1f340217..2a1f02a82 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -32,6 +32,7 @@ import ( . "github.com/scionproto/scion/verification/utils/definitions" sl "github.com/scionproto/scion/verification/utils/slices" + "github.com/scionproto/scion/verification/io" ) ghost const MutexPerm perm = 1/4 @@ -59,6 +60,7 @@ pred (d *DataPlane) Mem() { acc(&d.Metrics) && acc(&d.forwardingMetrics) && acc(&d.key) && + acc(&d.asid) && (d.external != nil ==> accBatchConn(d.external)) && (d.linkTypes != nil ==> acc(d.linkTypes)) && (d.neighborIAs != nil ==> acc(d.neighborIAs)) && @@ -71,7 +73,7 @@ pred (d *DataPlane) Mem() { acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && len(*d.key) > 0 && scrypto.ValidKeyForHash(*d.key) && - d.macFactory implements MacFactorySpec{d.key})) && + d.macFactory implements MacFactorySpec{d.key, d.asid})) && (d.bfdSessions != nil ==> accBfdSession(d.bfdSessions)) && (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && // The following permissions are enough to call all methods needed in fields @@ -149,10 +151,12 @@ pred (p *scionPacketProcessor) initMem() { // This is used as a signature, not as an assumed function. requires acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) requires scrypto.ValidKeyForHash(*key) +requires acc(asid, _) ensures acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) -ensures res != nil && res.Mem() +ensures h != nil && h.Mem() +ensures acc(asid, _) && sh === h && sh.Asid() == *asid decreases -func MacFactorySpec(ghost key *[]byte) (res hash.Hash) +func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.IO_as]) (h hash.Hash, ghost sh hash.ScionHashSpec) // useful to deal with incompletnesses pred hideLocalIA(p *addr.IA) { @@ -218,7 +222,7 @@ pure func (p *scionPacketProcessor) getIngressID() uint16 { ghost requires d.Mem() decreases -pure func (d *DataPlane) getMacFactory() func() hash.Hash { +pure func (d *DataPlane) getMacFactory() func() (hash.Hash, ghost hash.ScionHashSpec) { return unfolding d.Mem() in d.macFactory } @@ -423,10 +427,11 @@ func (d *DataPlane) getMacFactoryMem() { ghost requires acc(d.Mem(), _) && d.getMacFactory() != nil ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _) +ensures acc(&d.asid, _) && acc(d.asid, _) ensures acc(sl.Bytes(*d.key, 0, len(*d.key)), _) ensures scrypto.ValidKeyForHash(*d.key) ensures len(*d.key) > 0 -ensures d.macFactory implements MacFactorySpec{d.key} +ensures d.macFactory implements MacFactorySpec{d.key, d.asid} decreases func (d *DataPlane) getNewPacketProcessorFootprint() { unfold acc(d.Mem(), _) diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index e6d919041..bbb32f045 100644 --- a/router/dataplane_spec_test.gobra +++ b/router/dataplane_spec_test.gobra @@ -12,7 +12,8 @@ // See the License for the specific language governing permissions and // limitations under the License. -// +gobra +// TODO: Include again +// gobra package router diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index 65c820af8..83b2ca499 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -8,7 +8,13 @@ package hash -import "io" +// TODO: Remove completely as this is not used here anymore. +// import "io" + +// TODO: Maybe find a different solution s.t. we don't have to import that here; +// note that we can't define `ScionHashSpec` elsewhere as Gobra doesn't support +// embedding imported types yet. +import "github.com/scionproto/scion/verification/io" // Hash is the common interface implemented by all hash functions. // @@ -70,4 +76,18 @@ type Hash interface { ensures res >= 0 decreases BlockSize() (res int) +} + +type ScionHashSpec interface { + Hash + + // TODO: Might want to open an issue regarding that repeating `Mem` is necessary here? + pred Mem() + + ghost + // TODO: If `Asid` depends on `Mem()`, then we don't know whether the result + // may change after call to `FullMAC`. It also shouldn't be necessary + // requires Mem() + decreases + pure Asid() (ghost io.IO_as) } \ No newline at end of file From 66b57dbb907f4629e399f70b6f740680c80fc50b Mon Sep 17 00:00:00 2001 From: henriman Date: Wed, 9 Apr 2025 16:32:42 +0200 Subject: [PATCH 12/22] Save work --- router/dataplane.go | 21 +++++++++++++++------ router/dataplane_spec.gobra | 14 ++++++++++++++ verification/dependencies/hash/hash.gobra | 3 ++- 3 files changed, 31 insertions(+), 7 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 224ef336a..79b546dbb 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2844,7 +2844,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) // @ preserves acc(&p.mac, R20) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && ValidHashSpec(p.mac, p.macSpec, dp) // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2885,6 +2886,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ decreases func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) + // @ unfold ValidHashSpec(p.mac, p.macSpec, dp) + // @ defer fold ValidHashSpec(p.mac, p.macSpec, dp) fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/) // TODO: Remove assertion // @ assert p.macSpec.Asid() == dp.Asid() @@ -3833,8 +3836,14 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ !llIsNil && startLL == 0 && endLL == len(ub) // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) -// @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ requires acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() +// @ ensures acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() +// preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// NOTE: I think the problem isn't with any of these conjuncts directly; rather, +// this precondition leads to satisfying the precondition of verifyCurrentMAC, +// allowing the verification to proceed further, leading to the performance problems. +// requires acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ requires acc(&p.macSpec, R20) && ValidHashSpec(p.mac, p.macSpec, dp) // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -4079,7 +4088,7 @@ func (p *scionPacketProcessor) process( // @ requires sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ preserves acc(&p.mac, R10) // @ preserves p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() @@ -4100,7 +4109,7 @@ func (p *scionPacketProcessor) process( // contracts for IO-spec // @ requires p.scionLayer.EqPathType(p.rawPkt) // @ requires !slayers.IsSupportedPkt(p.rawPkt) -// @ requires p.d.DpAgreesWithSpec(dp) +// requires p.d.DpAgreesWithSpec(dp) // TODO: Might also want to require dp.Valid() // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{}) // @ ensures respr.OutPkt != nil ==> @@ -4166,7 +4175,7 @@ func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (re // @ preserves acc(&ohp.Info, R55) && acc(&ohp.FirstHop, R55) // @ preserves acc(&p.macBuffers.scionInput, R55) // @ preserves acc(&p.mac, R55) && p.mac != nil && p.mac.Mem() - // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() + // preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases // @ outline ( diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 2a1f02a82..ef0bdc8ad 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -742,3 +742,17 @@ pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] { domain(d.forwardingMetrics) : set[uint16]{} } + +// pred (sh hash.ScionHashSpec) Valid(h hash.Hash, dp DataPlaneSpec) { +// acc(sh) && h === sh && sh.Asid() == dp.Asid() +// } + +// ghost +// decreases +// pure func Valid(h hash.Hash, sh hash.ScionHashSpec, dp io.DataPlaneSpec) bool { +// h === sh && sh.Asid() == dp.Asid() +// } + +pred ValidHashSpec(h hash.Hash, sh hash.ScionHashSpec, dp io.DataPlaneSpec) { + h === sh && sh != nil && sh.Asid() == dp.Asid() +} \ No newline at end of file diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index 83b2ca499..20f457b5b 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -82,11 +82,12 @@ type ScionHashSpec interface { Hash // TODO: Might want to open an issue regarding that repeating `Mem` is necessary here? + // TODO: explain why this is necessary pred Mem() ghost // TODO: If `Asid` depends on `Mem()`, then we don't know whether the result - // may change after call to `FullMAC`. It also shouldn't be necessary + // may change after call to `FullMAC`. // requires Mem() decreases pure Asid() (ghost io.IO_as) From 8b397f8f7ecf2ad64aef8d4cdf75f1a82255d31d Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 1 Jul 2025 17:35:41 +0200 Subject: [PATCH 13/22] Apply name changes --- pkg/scrypto/scrypto_spec.gobra | 2 +- pkg/slayers/path/mac.go | 6 +++--- router/dataplane.go | 4 ++-- router/dataplane_spec.gobra | 2 +- verification/dependencies/hash/hash.gobra | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra index 12d80b36a..a93425855 100644 --- a/pkg/scrypto/scrypto_spec.gobra +++ b/pkg/scrypto/scrypto_spec.gobra @@ -44,4 +44,4 @@ ensures e == nil ==> ( sh.Asid() == asid) ensures e != nil ==> e.ErrorMem() decreases _ -func InitMac(key []byte, ghost asid io.IO_as) (h hash.Hash, ghost sh hash.ScionHashSpec, e error) +func InitMac(key []byte, ghost asid io.AS) (h hash.Hash, ghost sh hash.ScionHashSpec, e error) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index 27e7025e8..9561d03c0 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -34,7 +34,7 @@ const MACBufferSize = 16 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() && sh === h // @ ensures let absInf := info.ToAbsInfoField() in -// @ let absHF := hf.ToIO_HF() in +// @ let absHF := hf.Abs() in // @ let absMac := AbsMac(ret) in // @ absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases @@ -62,7 +62,7 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh h // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in // @ let absInf := info.ToAbsInfoField() in -// @ let absHF := hf.ToIO_HF() in +// @ let absHF := hf.Abs() in // @ let absMac := AbsMac(FromSliceToMacArray(res)) in // @ absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases @@ -86,7 +86,7 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost res = h.Sum(buffer[:0])[:16] // @ absInf := info.ToAbsInfoField() - // @ absHF := hf.ToIO_HF() + // @ absHF := hf.Abs() // @ absMac := AbsMac(FromSliceToMacArray(res)) // This is our "MAC assumption", linking the abstraction of the concrete MAC diff --git a/router/dataplane.go b/router/dataplane.go index d0ba3a2e6..2e49318c1 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -220,7 +220,7 @@ type DataPlane struct { // @ ghost key *[]byte // TODO: See if there is a way to circumvent storing `asid`, considering // that this can be generated from `localIA`. - // @ ghost asid gpointer[io.IO_as] + // @ ghost asid gpointer[io.AS] external map[uint16]BatchConn linkTypes map[uint16]topology.LinkType neighborIAs map[uint16]addr.IA @@ -346,7 +346,7 @@ func (d *DataPlane) SetKey(key []byte) (res error) { return alreadySet } - // @ ghost asid@ := io.IO_as{uint(d.localIA)} + // @ ghost asid@ := io.AS{uint(d.localIA)} // First check for MAC creation errors. if _ /*@, macSpec @*/, err := scrypto.InitMac(key /*@, asid @*/); err != nil { diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index ef0bdc8ad..82c7f7c3b 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -156,7 +156,7 @@ ensures acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) ensures h != nil && h.Mem() ensures acc(asid, _) && sh === h && sh.Asid() == *asid decreases -func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.IO_as]) (h hash.Hash, ghost sh hash.ScionHashSpec) +func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.AS]) (h hash.Hash, ghost sh hash.ScionHashSpec) // useful to deal with incompletnesses pred hideLocalIA(p *addr.IA) { diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index 20f457b5b..6f9acacf0 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -90,5 +90,5 @@ type ScionHashSpec interface { // may change after call to `FullMAC`. // requires Mem() decreases - pure Asid() (ghost io.IO_as) + pure Asid() (ghost io.AS) } \ No newline at end of file From 4cc5f11bbc63faeb8b6c8736ed5984786d7da9fc Mon Sep 17 00:00:00 2001 From: henriman Date: Wed, 30 Jul 2025 11:39:07 +0200 Subject: [PATCH 14/22] Make verify completely --- pkg/scrypto/scrypto_spec.gobra | 13 ++-- pkg/slayers/doc.go | 2 +- pkg/slayers/path/mac.go | 26 ++++---- pkg/slayers/scion_spec.gobra | 20 +++--- router/dataplane.go | 81 +++++++++++++++++++---- router/dataplane_spec.gobra | 36 +++++++--- router/dataplane_spec_test.gobra | 3 +- verification/dependencies/hash/hash.gobra | 26 +++++++- 8 files changed, 154 insertions(+), 53 deletions(-) diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra index b33787ac5..94f0da336 100644 --- a/pkg/scrypto/scrypto_spec.gobra +++ b/pkg/scrypto/scrypto_spec.gobra @@ -19,8 +19,11 @@ package scrypto -import "hash" -import sl "github.com/scionproto/scion/verification/utils/slices" +import ( + "hash" + sl "github.com/scionproto/scion/verification/utils/slices" + "github.com/scionproto/scion/verification/io" +) // The error returned by initMac is produced deterministically depending on the key. // If an initial call to initmac succeeds with a key, then any subsequent @@ -33,7 +36,9 @@ pure func ValidKeyForHash(key []byte) bool preserves acc(sl.Bytes(key, 0, len(key)), _) ensures old(ValidKeyForHash(key)) ==> e == nil -ensures e == nil ==> (h != nil && h.Mem() && ValidKeyForHash(key)) +ensures e == nil ==> ( + h != nil && h.Mem() && ValidKeyForHash(key) && + h === sh && sh.Asid() == asid) ensures e != nil ==> e.ErrorMem() decreases _ -func InitMac(key []byte) (h hash.Hash, e error) +func InitMac(key []byte, ghost asid io.AS) (h hash.Hash, ghost sh hash.ScionHashSpec, e error) diff --git a/pkg/slayers/doc.go b/pkg/slayers/doc.go index d27e24f6e..59c9844bb 100644 --- a/pkg/slayers/doc.go +++ b/pkg/slayers/doc.go @@ -63,7 +63,7 @@ even branching based on layer type... it'll handle an (scn, e2e, udp) or (scn, h Note: Great care has been taken to only lazily parse the SCION header, however, HBH and E2E extensions are currently eagerly parsed (if they exist). Thus, handling packets containing these -extensions will be much slower (see the package benchmarks for reference). +extensions will be much slower (see the Package benchmarks for reference). When using the DecodingLayerParser, the extensions can be explicitly skipped by using the HopByHop/EndToEndExtnSkipper layer. The content of this Skipper-layer can be decoded into the full representation when necessary. diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index 2c98df061..9561d03c0 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -30,16 +30,16 @@ const MACBufferSize = 16 // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. -// @ requires h != nil && h.Mem() +// @ requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() +// @ ensures h.Mem() && sh === h // @ ensures let absInf := info.ToAbsInfoField() in -// @ let absHF := hf.ToIO_HF() in +// @ let absHF := hf.Abs() in // @ let absMac := AbsMac(ret) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases -func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (ret [MacLen]byte) { - mac := FullMAC(h, info, hf, buffer /*@, as_ @*/) +func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh hash.ScionHashSpec @*/) (ret [MacLen]byte) { + mac := FullMAC(h, info, hf, buffer /*@, sh @*/) var res /*@@@*/ [MacLen]byte // @ unfold sl.Bytes(mac, 0, MACBufferSize) @@ -56,17 +56,17 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. // In contrast to MAC(), FullMAC returns all the 16 bytes instead of only 6 bytes of the MAC. -// @ requires h != nil && h.Mem() +// @ requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() +// @ ensures h.Mem() && sh === h // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in // @ let absInf := info.ToAbsInfoField() in -// @ let absHF := hf.ToIO_HF() in +// @ let absHF := hf.Abs() in // @ let absMac := AbsMac(FromSliceToMacArray(res)) in -// @ absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) +// @ absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo) // @ decreases -func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost as_ io.IO_as @*/) (res []byte) { +func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh hash.ScionHashSpec @*/) (res []byte) { if len(buffer) < MACBufferSize { buffer = make([]byte, MACBufferSize) // @ fold sl.Bytes(buffer, 0, len(buffer)) @@ -86,12 +86,12 @@ func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost res = h.Sum(buffer[:0])[:16] // @ absInf := info.ToAbsInfoField() - // @ absHF := hf.ToIO_HF() + // @ absHF := hf.Abs() // @ absMac := AbsMac(FromSliceToMacArray(res)) // This is our "MAC assumption", linking the abstraction of the concrete MAC // tag to the abstract computation of the MAC tag. - // @ AssumeForIO(absMac == io.nextMsgtermSpec(as_, absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) + // @ AssumeForIO(absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)) // @ fold sl.Bytes(res, 0, MACBufferSize) return res diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 4c04594cb..e1864ce5d 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -409,20 +409,20 @@ requires sl.Bytes(ub, 0, len(ub)) decreases pure func (s *SCION) EqAbsHeader(ub []byte) bool { return unfolding s.Mem(ub) in - let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in + let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in let high := s.HdrLen*LineLen in - GetAddressOffset(ub) == low && + GetAddressOffset(ub) == low_ && GetLength(ub) == int(high) && // Might be worth introducing EqAbsHeader as an interface method on Path // to avoid doing these casts, especially when we add support for EPIC. typeOf(s.Path) == (*scion.Raw) && - unfolding s.Path.Mem(ub[low:high]) in + unfolding s.Path.Mem(ub[low_:high]) in unfolding sl.Bytes(ub, 0, len(ub)) in - let _ := Asserting(forall k int :: {&ub[low:high][k]} 0 <= k && k < high ==> - &ub[low:high][k] == &ub[low + k]) in - let _ := Asserting(forall k int :: {&ub[low:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> - &ub[low:high][:scion.MetaLen][k] == &ub[low:high][k]) in - let metaHdr := scion.DecodedFrom(binary.BigEndian.Uint32(ub[low:high][:scion.MetaLen])) in + let _ := Asserting(forall k int :: {&ub[low_:high][k]} 0 <= k && k < high ==> + &ub[low_:high][k] == &ub[low_ + k]) in + let _ := Asserting(forall k int :: {&ub[low_:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> + &ub[low_:high][:scion.MetaLen][k] == &ub[low_:high][k]) in + let metaHdr := scion.DecodedFrom(binary.BigEndian.Uint32(ub[low_:high][:scion.MetaLen])) in let seg1 := int(metaHdr.SegLen[0]) in let seg2 := int(metaHdr.SegLen[1]) in let seg3 := int(metaHdr.SegLen[2]) in @@ -438,10 +438,10 @@ requires s.Mem(ub) decreases pure func (s *SCION) ValidScionInitSpec(ub []byte) bool { return unfolding s.Mem(ub) in - let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in + let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in let high := s.HdrLen*LineLen in typeOf(s.Path) == (*scion.Raw) && - s.Path.(*scion.Raw).GetBase(ub[low:high]).WeaklyValid() + s.Path.(*scion.Raw).GetBase(ub[low_:high]).WeaklyValid() } // Checks if the common path header is valid in the serialized scion packet. diff --git a/router/dataplane.go b/router/dataplane.go index bd40674e9..99cdd18f5 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -218,6 +218,9 @@ type DataPlane struct { // (VerifiedSCION) This is stored in the dataplane in order to retain // knowledge that macFactory will not fail. // @ ghost key *[]byte + // TODO: See if there is a way to circumvent storing `asid`, considering + // that this can be generated from `localIA`. + // @ ghost asid gpointer[io.AS] external map[uint16]BatchConn linkTypes map[uint16]topology.LinkType neighborIAs map[uint16]addr.IA @@ -225,7 +228,7 @@ type DataPlane struct { internalIP net.IP internalNextHops map[uint16]*net.UDPAddr svc *services - macFactory func() hash.Hash + macFactory func() (hash.Hash /*@, ghost hash.ScionHashSpec @*/) bfdSessions map[uint16]bfdSession localIA addr.IA mtx sync.Mutex @@ -274,6 +277,7 @@ func (e scmpError) Error() string { // @ requires !d.IsRunning() // @ requires d.LocalIA().IsZero() // @ requires !ia.IsZero() +// @ requires !d.KeyIsSet() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant! // @ ensures acc(d.Mem(), OutMutexPerm) @@ -342,22 +346,28 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // @ Unreachable() return alreadySet } + + // @ ghost var asid@ io.AS = io.AS{uint(d.localIA)} + // First check for MAC creation errors. - if _, err := scrypto.InitMac(key); err != nil { + if _ /*@, macSpec @*/, err := scrypto.InitMac(key /*@, asid @*/); err != nil { return err } // @ d.key = &key + // @ d.asid = &asid verScionTemp := // @ requires acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _) // @ requires scrypto.ValidKeyForHash(key) + // @ requires acc(&asid, _) // @ ensures acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _) // @ ensures h != nil && h.Mem() + // @ ensures acc(&asid, _) && sh === h && sh.Asid() == asid // @ decreases - func /*@ f @*/ () (h hash.Hash) { - mac, _ := scrypto.InitMac(key) - return mac + func /*@ f @*/ () (h hash.Hash /*@, ghost sh hash.ScionHashSpec @*/) { + mac /*@, macSpec @*/, _ := scrypto.InitMac(key /*@, asid @*/) + return mac /*@, macSpec @*/ } - // @ proof verScionTemp implements MacFactorySpec{d.key} { + // @ proof verScionTemp implements MacFactorySpec{d.key, d.asid} { // @ return verScionTemp() as f // @ } d.macFactory = verScionTemp @@ -546,6 +556,7 @@ func (d *DataPlane) AddExternalInterfaceBFD(ifID uint16, conn BatchConn, PacketsReceived: d.Metrics.BFDPacketsReceived.With(labels), } } + // TODO: Now that macFactory returns two values, might want to move this call out? s := newBFDSend(conn, src.IA, dst.IA, src.Addr, dst.Addr, ifID, d.macFactory()) return d.addBFDController(ifID, s, cfg, m) } @@ -764,7 +775,7 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro PacketsReceived: d.Metrics.SiblingBFDPacketsReceived.With(labels), } } - + // TODO: Now that macFactory returns two values, might want to move this call out? s := newBFDSend(d.internal, d.localIA, d.localIA, src, dst, 0, d.macFactory()) return d.addBFDController(ifID, s, cfg, m) } @@ -921,6 +932,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant d.getValForwardingMetrics() != nil // @ invariant 0 in d.getDomForwardingMetrics() // @ invariant ingressID in d.getDomForwardingMetrics() + // @ invariant d.KeyIsSet() // @ invariant acc(rd.Mem(), _) // @ invariant processor.sInit() && processor.sInitD() === d // @ invariant let ubuf := processor.sInitBufferUBuf() in @@ -993,6 +1005,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant d.getValForwardingMetrics() != nil // @ invariant 0 in d.getDomForwardingMetrics() // @ invariant ingressID in d.getDomForwardingMetrics() + // @ invariant d.KeyIsSet() // @ invariant acc(rd.Mem(), _) // @ invariant pkts <= len(msgs) // @ invariant 0 <= i0 && i0 <= pkts @@ -1435,19 +1448,29 @@ type processResult struct { // @ decreases func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcessor) { var verScionTmp gopacket.SerializeBuffer + // unfold acc(d.Mem(), _) + // assert d.localIA == d.LocalIA() // @ d.getNewPacketProcessorFootprint() + // assert d.macFactory implements MacFactorySpec{d.key, d.asid} + // assert d.localIA == d.LocalIA() + // assert io.AS{uint(d.localIA)} == io.AS{uint(d.LocalIA())} verScionTmp = gopacket.NewSerializeBuffer() // @ sl.PermsImplyIneqWithWildcard(verScionTmp.UBuf(), *d.key) + mac /*@, macSpec @*/ := (d.macFactory() /*@ as MacFactorySpec{d.key, d.asid} @*/) p := &scionPacketProcessor{ d: d, ingressID: ingressID, buffer: verScionTmp, - mac: (d.macFactory() /*@ as MacFactorySpec{d.key} @ */), + mac: mac, macBuffers: macBuffersT{ scionInput: make([]byte, path.MACBufferSize), epicInput: make([]byte, libepic.MACBufferSize), }, } + // TODO: Doing this "right in initialization" makes Gobra think `p` is a + // TODO: should it be a gpointer? + // `gpointer` and not a "normal" pointer. + // @ p.macSpec = macSpec // @ fold sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw) p.scionLayer.RecyclePaths() @@ -1496,7 +1519,8 @@ func (p *scionPacketProcessor) reset() (err error) { // @ d.WellConfigured() && // @ d.getValSvc() != nil && // @ d.getValForwardingMetrics() != nil && -// @ d.DpAgreesWithSpec(dp) +// @ d.DpAgreesWithSpec(dp) && +// @ d.KeyIsSet() // @ requires let ubuf := p.sInitBufferUBuf() in // @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ ensures p.sInit() @@ -1636,9 +1660,19 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ unfold acc(p.d.Mem(), _) + // @ assert p.d.macFactory != nil + // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt)) - v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP( /*@ dp @*/ ) + // TODO: we seem to be going over three "corners" here, maybe that can be improved + // @ reveal p.d.DpAgreesWithSpec(dp) + // @ assert p.d.dpSpecWellConfiguredLocalIA(dp) + // @ assert dp.Asid() == io.AS{uint(p.d.localIA)} + // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} + // @ assert dp.Asid() == *p.d.asid + // @ assert p.macSpec.Asid() == *p.d.asid + // @ assert p.macSpec.Asid() == dp.Asid() + v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP(/*@ dp @*/) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() return v1, v2 /*@, aliasesPkt, newAbsPkt @*/ @@ -1649,6 +1683,17 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm) // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) + // TODO: minimize assertions etc. + // @ unfold acc(p.d.Mem(), _) + // @ assert p.d.macFactory != nil + // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} + // @ reveal p.d.DpAgreesWithSpec(dp) + // @ assert p.d.dpSpecWellConfiguredLocalIA(dp) + // @ assert dp.Asid() == io.AS{uint(p.d.localIA)} + // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} + // @ assert dp.Asid() == *p.d.asid + // @ assert p.macSpec.Asid() == *p.d.asid + // @ assert p.macSpec.Asid() == dp.Asid() v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1798,6 +1843,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -1920,6 +1966,9 @@ type scionPacketProcessor struct { buffer gopacket.SerializeBuffer // mac is the hasher for the MAC computation. mac hash.Hash + // `macSpec` lets us access the AS identifier corresponding to the private + // key used by `mac`. + // @ ghost macSpec hash.ScionHashSpec // scionLayer is the SCION gopacket layer. scionLayer slayers.SCION @@ -2857,6 +2906,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) // @ preserves acc(&p.mac, R20) && p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2897,7 +2947,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ decreases func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) - fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, dp.Asid() @*/) + fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { @@ -3837,6 +3887,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -4081,6 +4132,7 @@ func (p *scionPacketProcessor) process( // @ requires sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ preserves acc(&p.mac, R10) // @ preserves p.mac != nil && p.mac.Mem() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() @@ -4106,7 +4158,7 @@ func (p *scionPacketProcessor) process( // @ newAbsPkt == absIO_val(respr.OutPkt, respr.EgressID) && // @ newAbsPkt.isValUnsupported // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { +func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { // @ ghost ubScionL := p.rawPkt // @ p.scionLayer.ExtractAcc(ubScionL) s := p.scionLayer @@ -4165,10 +4217,11 @@ func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) ( // @ preserves acc(&ohp.Info, R55) && acc(&ohp.FirstHop, R55) // @ preserves acc(&p.macBuffers.scionInput, R55) // @ preserves acc(&p.mac, R55) && p.mac != nil && p.mac.Mem() + // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases // @ outline ( - mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput /*@, dp.Asid() @*/) + mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput /*@, p.macSpec @*/) // (VerifiedSCION) introduced separate copy to avoid exposing quantified permissions outside the scope of this outline block. macCopy := mac // @ fold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56) @@ -4245,7 +4298,7 @@ func (p *scionPacketProcessor) processOHP( /*@ ghost dp io.DataPlaneSpec @*/ ) ( // XXX(roosd): Here we leak the buffer into the SCION packet header. // This is okay because we do not operate on the buffer or the packet // for the rest of processing. - ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput /*@, dp.Asid() @*/) + ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput /*@, p.macSpec @*/) // @ fold ohp.SecondHop.Mem() // @ fold s.Path.Mem(ubPath) // @ fold acc(p.scionLayer.Mem(ubScionL), 1-R15) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index e1f340217..7a48754fd 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -32,6 +32,7 @@ import ( . "github.com/scionproto/scion/verification/utils/definitions" sl "github.com/scionproto/scion/verification/utils/slices" + "github.com/scionproto/scion/verification/io" ) ghost const MutexPerm perm = 1/4 @@ -59,6 +60,7 @@ pred (d *DataPlane) Mem() { acc(&d.Metrics) && acc(&d.forwardingMetrics) && acc(&d.key) && + acc(&d.asid) && (d.external != nil ==> accBatchConn(d.external)) && (d.linkTypes != nil ==> acc(d.linkTypes)) && (d.neighborIAs != nil ==> acc(d.neighborIAs)) && @@ -67,11 +69,13 @@ pred (d *DataPlane) Mem() { (d.internalNextHops != nil ==> accAddr(d.internalNextHops)) && (d.svc != nil ==> d.svc.Mem()) && (d.macFactory != nil ==> ( - acc(d.key) && - acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && - len(*d.key) > 0 && - scrypto.ValidKeyForHash(*d.key) && - d.macFactory implements MacFactorySpec{d.key})) && + // TODO: probably also need ac(d.asid) + acc(d.key) && + acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && + len(*d.key) > 0 && + scrypto.ValidKeyForHash(*d.key) && + acc(d.asid) && *d.asid == io.AS{uint(d.localIA)} && + d.macFactory implements MacFactorySpec{d.key, d.asid})) && (d.bfdSessions != nil ==> accBfdSession(d.bfdSessions)) && (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && // The following permissions are enough to call all methods needed in fields @@ -149,10 +153,12 @@ pred (p *scionPacketProcessor) initMem() { // This is used as a signature, not as an assumed function. requires acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) requires scrypto.ValidKeyForHash(*key) +requires acc(asid, _) ensures acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) -ensures res != nil && res.Mem() +ensures h != nil && h.Mem() +ensures acc(asid, _) && sh === h && sh.Asid() == *asid decreases -func MacFactorySpec(ghost key *[]byte) (res hash.Hash) +func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.AS]) (h hash.Hash, ghost sh hash.ScionHashSpec) // useful to deal with incompletnesses pred hideLocalIA(p *addr.IA) { @@ -218,7 +224,7 @@ pure func (p *scionPacketProcessor) getIngressID() uint16 { ghost requires d.Mem() decreases -pure func (d *DataPlane) getMacFactory() func() hash.Hash { +pure func (d *DataPlane) getMacFactory() func() (hash.Hash, ghost hash.ScionHashSpec) { return unfolding d.Mem() in d.macFactory } @@ -423,10 +429,12 @@ func (d *DataPlane) getMacFactoryMem() { ghost requires acc(d.Mem(), _) && d.getMacFactory() != nil ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _) +// ensures acc(&d.asid, _) && acc(d.asid, _) ensures acc(sl.Bytes(*d.key, 0, len(*d.key)), _) ensures scrypto.ValidKeyForHash(*d.key) ensures len(*d.key) > 0 -ensures d.macFactory implements MacFactorySpec{d.key} +ensures acc(&d.asid, _) && acc(d.asid, _) +ensures d.macFactory implements MacFactorySpec{d.key, d.asid} decreases func (d *DataPlane) getNewPacketProcessorFootprint() { unfold acc(d.Mem(), _) @@ -573,6 +581,16 @@ pred (s* scionPacketProcessor) sInit() { acc(&s.buffer) && s.buffer != nil && s.buffer.Mem() && acc(&s.mac) && s.mac != nil && s.mac.Mem() && + // TODO: see if there is a more sensible place for this + acc(&s.macSpec) && acc(&s.d.asid, _) && acc(s.d.asid, _) && + s.mac === s.macSpec && + s.macSpec.Asid() == *s.d.asid && + // TODO: Problem: We don't have access to *s.d, only s.d + // We can only access it together with access to the DataPlane + // (and the fact that it is the same as s.d), so we have to + // put that information elsewhere + // acc(&s.d.localIA) && + // s.macSpec.Asid() == io.AS{uint(s.d.localIA)} && s.scionLayer.NonInitMem() && // The following is not necessary // s.scionLayer.PathPoolInitializedNonInitMem() && diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index 241d8386e..a87d0ed47 100644 --- a/router/dataplane_spec_test.gobra +++ b/router/dataplane_spec_test.gobra @@ -12,7 +12,8 @@ // See the License for the specific language governing permissions and // limitations under the License. -// +gobra +// TODO: include again +// gobra package router diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index 65c820af8..1812b75ac 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -8,7 +8,13 @@ package hash -import "io" +// TODO: Remove as this is not used here anymore (and clashes with our `io`) +// import "io" + +// TODO: Maybe find a different solution s.t. we don't have to import that here; +// note that we can't define `ScionHashSpec` elsewhere as Gobra doesn't support +// embedding imported types yet. +import "github.com/scionproto/scion/verification/io" // Hash is the common interface implemented by all hash functions. // @@ -70,4 +76,22 @@ type Hash interface { ensures res >= 0 decreases BlockSize() (res int) +} + +// TODO: Explain need for ScionHashSpec +type ScionHashSpec interface { + Hash + + // Due to a bug (?) in Gobra, this needs to be repeated here. + // TODO: Check again whether this is a bug, if so open an issue and update + // the comment here to refer to it. + pred Mem() + + ghost + // TODO: If `Asid` depends on `Mem()`, then we don't know whether the result + // may change after call to `FullMAC` (as it consumes `Mem`). + // However, we likely don't need to require `Mem` here anyway. + // requires Mem() + decreases + pure Asid() (ghost io.AS) } \ No newline at end of file From 7d2af9b8e744957e2db01cf90ca9237ccbd6ffb4 Mon Sep 17 00:00:00 2001 From: henriman Date: Fri, 8 Aug 2025 11:05:52 +0200 Subject: [PATCH 15/22] Save work --- router/dataplane.go | 4 ++++ verification/dependencies/hash/hash.gobra | 11 ++++++++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 99cdd18f5..f89a805a5 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -4217,6 +4217,10 @@ func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (re // @ preserves acc(&ohp.Info, R55) && acc(&ohp.FirstHop, R55) // @ preserves acc(&p.macBuffers.scionInput, R55) // @ preserves acc(&p.mac, R55) && p.mac != nil && p.mac.Mem() + // NOTE[henri]: We don't need `p.macSpec.Asid() == dp.Asid()` *yet*, + // however we definitely will eventually (to be able to declassify `mac` + // s.t. `compRes` / the branch condition is low). + // Should I keep this in already anyway? // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index 1812b75ac..f6c5e97ea 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -88,9 +88,14 @@ type ScionHashSpec interface { pred Mem() ghost - // TODO: If `Asid` depends on `Mem()`, then we don't know whether the result - // may change after call to `FullMAC` (as it consumes `Mem`). - // However, we likely don't need to require `Mem` here anyway. + // NOTE[henri]: If `Asid` depends on `Mem()`, then we don't know whether + // the result may change after a call to `FullMAC` (as it consumes `Mem`). + // While we could add a respective postcondition to `FullMAC`, I'm not sure + // how to go about proving this postcondition, since (I think) we would need + // to add contracts to `Hash.Write` and `Hash.Reset` that specify that + // the result of `Asid()` does not change -- but we cannot access `Asid()` + // in `Hash`, only in `ScionHashSpec` (right?) + // Do we even need `requires Mem()`? // requires Mem() decreases pure Asid() (ghost io.AS) From 7665ae4861cc18b6a95b7bfda5baf61b43ff496e Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 19 Aug 2025 12:26:50 +0200 Subject: [PATCH 16/22] Save work --- pkg/scrypto/scrypto_spec.gobra | 3 ++- pkg/slayers/path/mac.go | 12 ++++++--- router/dataplane.go | 14 +++++----- router/dataplane_spec.gobra | 5 ++-- verification/dependencies/hash/hash.gobra | 32 ++++++++++++++--------- 5 files changed, 40 insertions(+), 26 deletions(-) diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra index 94f0da336..dea8a7c18 100644 --- a/pkg/scrypto/scrypto_spec.gobra +++ b/pkg/scrypto/scrypto_spec.gobra @@ -38,7 +38,8 @@ preserves acc(sl.Bytes(key, 0, len(key)), _) ensures old(ValidKeyForHash(key)) ==> e == nil ensures e == nil ==> ( h != nil && h.Mem() && ValidKeyForHash(key) && - h === sh && sh.Asid() == asid) + // h === sh && sh.Asid() == asid) + h === sh && sh.AsidMem() && sh.Asid() == asid) ensures e != nil ==> e.ErrorMem() decreases _ func InitMac(key []byte, ghost asid io.AS) (h hash.Hash, ghost sh hash.ScionHashSpec, e error) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index 9561d03c0..56a01789e 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -30,9 +30,11 @@ const MACBufferSize = 16 // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. -// @ requires h != nil && h.Mem() && sh === h +// @ requires h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) +// requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() && sh === h +// @ ensures h.Mem() && sh === h && sh.AsidMem() +// ensures h.Mem() && sh === h // @ ensures let absInf := info.ToAbsInfoField() in // @ let absHF := hf.Abs() in // @ let absMac := AbsMac(ret) in @@ -56,9 +58,11 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh h // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. // In contrast to MAC(), FullMAC returns all the 16 bytes instead of only 6 bytes of the MAC. -// @ requires h != nil && h.Mem() && sh === h +// @ requires h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) +// requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() && sh === h +// @ ensures h.Mem() && sh === h && sh.AsidMem() +// ensures h.Mem() && sh === h // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in // @ let absInf := info.ToAbsInfoField() in diff --git a/router/dataplane.go b/router/dataplane.go index f89a805a5..8a6420816 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -361,7 +361,8 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // @ requires acc(&asid, _) // @ ensures acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _) // @ ensures h != nil && h.Mem() - // @ ensures acc(&asid, _) && sh === h && sh.Asid() == asid + // @ ensures acc(&asid, _) && sh === h && sh.AsidMem() && sh.Asid() == asid + // ensures acc(&asid, _) && sh === h && sh.Asid() == asid // @ decreases func /*@ f @*/ () (h hash.Hash /*@, ghost sh hash.ScionHashSpec @*/) { mac /*@, macSpec @*/, _ := scrypto.InitMac(key /*@, asid @*/) @@ -1843,7 +1844,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2906,7 +2907,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) // @ preserves acc(&p.mac, R20) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2948,6 +2949,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/) + // @ assert p.macSpec.Asid() == old(p.macSpec.Asid()) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { @@ -3887,7 +3889,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -4132,7 +4134,7 @@ func (p *scionPacketProcessor) process( // @ requires sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ preserves acc(&p.mac, R10) // @ preserves p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() @@ -4221,7 +4223,7 @@ func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (re // however we definitely will eventually (to be able to declassify `mac` // s.t. `compRes` / the branch condition is low). // Should I keep this in already anyway? - // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.Asid() == dp.Asid() + // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases // @ outline ( diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 7a48754fd..7dff5625b 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -156,7 +156,8 @@ requires scrypto.ValidKeyForHash(*key) requires acc(asid, _) ensures acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) ensures h != nil && h.Mem() -ensures acc(asid, _) && sh === h && sh.Asid() == *asid +ensures acc(asid, _) && sh === h && sh.AsidMem() && sh.Asid() == *asid +// ensures acc(asid, _) && sh === h && sh.Asid() == *asid decreases func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.AS]) (h hash.Hash, ghost sh hash.ScionHashSpec) @@ -584,7 +585,7 @@ pred (s* scionPacketProcessor) sInit() { // TODO: see if there is a more sensible place for this acc(&s.macSpec) && acc(&s.d.asid, _) && acc(s.d.asid, _) && s.mac === s.macSpec && - s.macSpec.Asid() == *s.d.asid && + s.macSpec.AsidMem() && s.macSpec.Asid() == *s.d.asid && // TODO: Problem: We don't have access to *s.d, only s.d // We can only access it together with access to the DataPlane // (and the fact that it is the same as s.d), so we have to diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index f6c5e97ea..ac93efbb3 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -35,6 +35,9 @@ import "github.com/scionproto/scion/verification/io" type Hash interface { pred Mem() + // Due to Gobra issue #959, we need to repeat `pred AsidMem()` here. + pred AsidMem() + // Write (via the embedded io.Writer interface) adds more data to the running hash. // It never returns an error. @@ -78,25 +81,28 @@ type Hash interface { BlockSize() (res int) } -// TODO: Explain need for ScionHashSpec +// In order to adequately relate the abstract computation of a MAC tag (using +// `io.nextMsgtermSpec`) to the concrete computation (using `path.FullMAC` and +// `path.MAC`), we need to relate the key used by `io.nextMsgtermSpec` -- which +// is simply "indexed" by the AS identifier -- to the key used by the `Hash` +// instance passed to `path.FullMAC`/`path.MAC` (VerifiedSCION uses a keyed hash). +// To this end, during the creation of the `Hash` instance, we not only pass +// the key but also the associated AS ID (cf. `scrypto.InitMac`) which can then +// later be accessed using `Asid()`. +// As this specification is specific to VerifiedSCION, we don't add it to `Hash` +// directly, but instead in this interface which embeds `Hash`. type ScionHashSpec interface { Hash - // Due to a bug (?) in Gobra, this needs to be repeated here. - // TODO: Check again whether this is a bug, if so open an issue and update - // the comment here to refer to it. + // Due to Gobra issue #958, we need to repeat `pred Mem()` here. pred Mem() + // Memory footprint for `Asid`. Needed s.t. we can establish that the result + // of `Asid()` does not change after a call to `Write` or `Reset`. + pred AsidMem() + ghost - // NOTE[henri]: If `Asid` depends on `Mem()`, then we don't know whether - // the result may change after a call to `FullMAC` (as it consumes `Mem`). - // While we could add a respective postcondition to `FullMAC`, I'm not sure - // how to go about proving this postcondition, since (I think) we would need - // to add contracts to `Hash.Write` and `Hash.Reset` that specify that - // the result of `Asid()` does not change -- but we cannot access `Asid()` - // in `Hash`, only in `ScionHashSpec` (right?) - // Do we even need `requires Mem()`? - // requires Mem() + requires AsidMem() decreases pure Asid() (ghost io.AS) } \ No newline at end of file From 291a0c7cb9161f0cabe84b21210980c574c88eb0 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 6 Oct 2025 16:17:57 +0200 Subject: [PATCH 17/22] Finish introducing AsidMem --- pkg/slayers/path/mac.go | 4 ++-- router/dataplane.go | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index 56a01789e..b0aa1696a 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -33,7 +33,7 @@ const MACBufferSize = 16 // @ requires h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) // requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() && sh === h && sh.AsidMem() +// @ ensures h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) // ensures h.Mem() && sh === h // @ ensures let absInf := info.ToAbsInfoField() in // @ let absHF := hf.Abs() in @@ -61,7 +61,7 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh h // @ requires h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) // requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) -// @ ensures h.Mem() && sh === h && sh.AsidMem() +// @ ensures h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) // ensures h.Mem() && sh === h // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in diff --git a/router/dataplane.go b/router/dataplane.go index 2352c1fb5..910f15215 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1521,7 +1521,7 @@ func (p *scionPacketProcessor) reset() (err error) { // @ d.getValSvc() != nil && // @ d.getValForwardingMetrics() != nil && // @ d.DpAgreesWithSpec(dp) && -// @ d.KeyIsSet() +// @ d.KeyIsSet() // @ requires let ubuf := p.sInitBufferUBuf() in // @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ ensures p.sInit() From 985c46a1ffe53d2c78d40adfb991366c7baca437 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 6 Oct 2025 16:45:20 +0200 Subject: [PATCH 18/22] General clean-up --- pkg/scrypto/scrypto_spec.gobra | 1 - pkg/slayers/path/mac.go | 4 -- router/dataplane.go | 37 +++++++------------ router/dataplane_spec.gobra | 32 ++++++---------- router/dataplane_spec_test.gobra | 2 +- .../crypto/subtle/constant_time.gobra | 4 +- verification/dependencies/hash/hash.gobra | 8 +--- 7 files changed, 30 insertions(+), 58 deletions(-) diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra index dea8a7c18..c3fef85d4 100644 --- a/pkg/scrypto/scrypto_spec.gobra +++ b/pkg/scrypto/scrypto_spec.gobra @@ -38,7 +38,6 @@ preserves acc(sl.Bytes(key, 0, len(key)), _) ensures old(ValidKeyForHash(key)) ==> e == nil ensures e == nil ==> ( h != nil && h.Mem() && ValidKeyForHash(key) && - // h === sh && sh.Asid() == asid) h === sh && sh.AsidMem() && sh.Asid() == asid) ensures e != nil ==> e.ErrorMem() decreases _ diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go index b0aa1696a..1c8ef5637 100644 --- a/pkg/slayers/path/mac.go +++ b/pkg/slayers/path/mac.go @@ -31,10 +31,8 @@ const MACBufferSize = 16 // this method does not modify info or hf. // Modifying the provided buffer after calling this function may change the returned HopField MAC. // @ requires h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) -// requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) -// ensures h.Mem() && sh === h // @ ensures let absInf := info.ToAbsInfoField() in // @ let absHF := hf.Abs() in // @ let absMac := AbsMac(ret) in @@ -59,10 +57,8 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh h // Modifying the provided buffer after calling this function may change the returned HopField MAC. // In contrast to MAC(), FullMAC returns all the 16 bytes instead of only 6 bytes of the MAC. // @ requires h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) -// requires h != nil && h.Mem() && sh === h // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer)) // @ ensures h.Mem() && sh === h && acc(sh.AsidMem(), 1/2) -// ensures h.Mem() && sh === h // @ ensures len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize) // @ ensures unfolding sl.Bytes(res, 0, MACBufferSize) in // @ let absInf := info.ToAbsInfoField() in diff --git a/router/dataplane.go b/router/dataplane.go index 910f15215..7c28c21c6 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -218,8 +218,6 @@ type DataPlane struct { // (VerifiedSCION) This is stored in the dataplane in order to retain // knowledge that macFactory will not fail. // @ ghost key *[]byte - // TODO: See if there is a way to circumvent storing `asid`, considering - // that this can be generated from `localIA`. // @ ghost asid gpointer[io.AS] external map[uint16]BatchConn linkTypes map[uint16]topology.LinkType @@ -362,7 +360,6 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // @ ensures acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _) // @ ensures h != nil && h.Mem() // @ ensures acc(&asid, _) && sh === h && sh.AsidMem() && sh.Asid() == asid - // ensures acc(&asid, _) && sh === h && sh.Asid() == asid // @ decreases func /*@ f @*/ () (h hash.Hash /*@, ghost sh hash.ScionHashSpec @*/) { mac /*@, macSpec @*/, _ := scrypto.InitMac(key /*@, asid @*/) @@ -557,7 +554,6 @@ func (d *DataPlane) AddExternalInterfaceBFD(ifID uint16, conn BatchConn, PacketsReceived: d.Metrics.BFDPacketsReceived.With(labels), } } - // TODO: Now that macFactory returns two values, might want to move this call out? s := newBFDSend(conn, src.IA, dst.IA, src.Addr, dst.Addr, ifID, d.macFactory()) return d.addBFDController(ifID, s, cfg, m) } @@ -776,7 +772,6 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro PacketsReceived: d.Metrics.SiblingBFDPacketsReceived.With(labels), } } - // TODO: Now that macFactory returns two values, might want to move this call out? s := newBFDSend(d.internal, d.localIA, d.localIA, src, dst, 0, d.macFactory()) return d.addBFDController(ifID, s, cfg, m) } @@ -1449,12 +1444,7 @@ type processResult struct { // @ decreases func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcessor) { var verScionTmp gopacket.SerializeBuffer - // unfold acc(d.Mem(), _) - // assert d.localIA == d.LocalIA() // @ d.getNewPacketProcessorFootprint() - // assert d.macFactory implements MacFactorySpec{d.key, d.asid} - // assert d.localIA == d.LocalIA() - // assert io.AS{uint(d.localIA)} == io.AS{uint(d.LocalIA())} verScionTmp = gopacket.NewSerializeBuffer() // @ sl.PermsImplyIneqWithWildcard(verScionTmp.UBuf(), *d.key) mac /*@, macSpec @*/ := (d.macFactory() /*@ as MacFactorySpec{d.key, d.asid} @*/) @@ -1468,9 +1458,6 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess epicInput: make([]byte, libepic.MACBufferSize), }, } - // TODO: Doing this "right in initialization" makes Gobra think `p` is a - // TODO: should it be a gpointer? - // `gpointer` and not a "normal" pointer. // @ p.macSpec = macSpec // @ fold sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw) @@ -1661,11 +1648,11 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ unfold acc(p.d.Mem(), _) + // TODO[henri]: minimize assertions // @ assert p.d.macFactory != nil // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt)) - // TODO: we seem to be going over three "corners" here, maybe that can be improved // @ reveal p.d.DpAgreesWithSpec(dp) // @ assert p.d.dpSpecWellConfiguredLocalIA(dp) // @ assert dp.Asid() == io.AS{uint(p.d.localIA)} @@ -1684,7 +1671,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm) // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) - // TODO: minimize assertions etc. + // TODO[henri]: minimize assertions // @ unfold acc(p.d.Mem(), _) // @ assert p.d.macFactory != nil // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} @@ -1844,7 +1831,8 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && +// @ p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2907,7 +2895,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) // @ preserves acc(&p.mac, R20) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && +// @ p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -2949,6 +2938,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/) + // TODO[henri]: might be able to remove this assertion // @ assert p.macSpec.Asid() == old(p.macSpec.Asid()) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) @@ -3889,7 +3879,8 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && +// @ p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) @@ -4134,7 +4125,8 @@ func (p *scionPacketProcessor) process( // @ requires sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ preserves acc(&p.mac, R10) // @ preserves p.mac != nil && p.mac.Mem() -// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() +// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && +// @ p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() @@ -4219,11 +4211,8 @@ func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (re // @ preserves acc(&ohp.Info, R55) && acc(&ohp.FirstHop, R55) // @ preserves acc(&p.macBuffers.scionInput, R55) // @ preserves acc(&p.mac, R55) && p.mac != nil && p.mac.Mem() - // NOTE[henri]: We don't need `p.macSpec.Asid() == dp.Asid()` *yet*, - // however we definitely will eventually (to be able to declassify `mac` - // s.t. `compRes` / the branch condition is low). - // Should I keep this in already anyway? - // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() + // @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && + // @ p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid() // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ decreases // @ outline ( diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 2bf1a42ab..0769b38ae 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -60,7 +60,7 @@ pred (d *DataPlane) Mem() { acc(&d.Metrics) && acc(&d.forwardingMetrics) && acc(&d.key) && - acc(&d.asid) && + acc(&d.asid) && (d.external != nil ==> accBatchConn(d.external)) && (d.linkTypes != nil ==> acc(d.linkTypes)) && (d.neighborIAs != nil ==> acc(d.neighborIAs)) && @@ -69,13 +69,12 @@ pred (d *DataPlane) Mem() { (d.internalNextHops != nil ==> accAddr(d.internalNextHops)) && (d.svc != nil ==> d.svc.Mem()) && (d.macFactory != nil ==> ( - // TODO: probably also need ac(d.asid) - acc(d.key) && - acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && - len(*d.key) > 0 && - scrypto.ValidKeyForHash(*d.key) && - acc(d.asid) && *d.asid == io.AS{uint(d.localIA)} && - d.macFactory implements MacFactorySpec{d.key, d.asid})) && + acc(d.key) && + acc(sl.Bytes(*d.key, 0, len(*d.key)), _) && + len(*d.key) > 0 && + scrypto.ValidKeyForHash(*d.key) && + acc(d.asid) && *d.asid == io.AS{uint(d.localIA)} && + d.macFactory implements MacFactorySpec{d.key, d.asid})) && (d.bfdSessions != nil ==> accBfdSession(d.bfdSessions)) && (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && // The following permissions are enough to call all methods needed in fields @@ -157,7 +156,6 @@ requires acc(asid, _) ensures acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _) ensures h != nil && h.Mem() ensures acc(asid, _) && sh === h && sh.AsidMem() && sh.Asid() == *asid -// ensures acc(asid, _) && sh === h && sh.Asid() == *asid decreases func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.AS]) (h hash.Hash, ghost sh hash.ScionHashSpec) @@ -423,7 +421,6 @@ func (d *DataPlane) getInternal() { ghost requires acc(d.Mem(), _) && d.getMacFactory() != nil ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _) -// ensures acc(&d.asid, _) && acc(d.asid, _) ensures acc(sl.Bytes(*d.key, 0, len(*d.key)), _) ensures scrypto.ValidKeyForHash(*d.key) ensures len(*d.key) > 0 @@ -574,16 +571,11 @@ pred (s* scionPacketProcessor) sInit() { acc(&s.buffer) && s.buffer != nil && s.buffer.Mem() && acc(&s.mac) && s.mac != nil && s.mac.Mem() && - // TODO: see if there is a more sensible place for this - acc(&s.macSpec) && acc(&s.d.asid, _) && acc(s.d.asid, _) && - s.mac === s.macSpec && - s.macSpec.AsidMem() && s.macSpec.Asid() == *s.d.asid && - // TODO: Problem: We don't have access to *s.d, only s.d - // We can only access it together with access to the DataPlane - // (and the fact that it is the same as s.d), so we have to - // put that information elsewhere - // acc(&s.d.localIA) && - // s.macSpec.Asid() == io.AS{uint(s.d.localIA)} && + acc(&s.macSpec) && + acc(&s.d.asid, _) && acc(s.d.asid, _) && + s.mac === s.macSpec && + s.macSpec.AsidMem() && + s.macSpec.Asid() == *s.d.asid && s.scionLayer.NonInitMem() && // The following is not necessary // s.scionLayer.PathPoolInitializedNonInitMem() && diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index 5f349cacf..8af8b2618 100644 --- a/router/dataplane_spec_test.gobra +++ b/router/dataplane_spec_test.gobra @@ -12,7 +12,7 @@ // See the License for the specific language governing permissions and // limitations under the License. -// TODO: include again +// TODO: Include this file in the verification again. // gobra package router diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra index 8635d9a78..e1330daf3 100644 --- a/verification/dependencies/crypto/subtle/constant_time.gobra +++ b/verification/dependencies/crypto/subtle/constant_time.gobra @@ -18,8 +18,8 @@ trusted requires sl.Bytes(x, 0, len(x)) requires sl.Bytes(y, 0, len(y)) ensures len(x) != len(y) ==> res == 0 -ensures res != 0 ==> +ensures res != 0 ==> forall i int :: { sl.GetByte(x, 0, len(x), i) }{ sl.GetByte(y, 0, len(y), i) } 0 <= i && i < len(x) ==> - sl.GetByte(x, 0, len(x), i) == sl.GetByte(y, 0, len(y), i) + sl.GetByte(x, 0, len(x), i) == sl.GetByte(y, 0, len(y), i) decreases pure func ConstantTimeCompare(x, y []byte) (res int) diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra index da0fca577..e8c23f096 100644 --- a/verification/dependencies/hash/hash.gobra +++ b/verification/dependencies/hash/hash.gobra @@ -8,12 +8,8 @@ package hash -// TODO: Remove as this is not used here anymore (and clashes with our `io`) -// import "io" - -// TODO: Maybe find a different solution s.t. we don't have to import that here; -// note that we can't define `ScionHashSpec` elsewhere as Gobra doesn't support -// embedding imported types yet. +// As Gobra doesn't support embedding imported types yet, we have to define +// `ScionHashSpec` here; consequently, there is no way around importing `io`. import "github.com/scionproto/scion/verification/io" // Hash is the common interface implemented by all hash functions. From 47d42235f5be6a17555dba0b03aa19d5558b3ea7 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 6 Oct 2025 17:27:07 +0200 Subject: [PATCH 19/22] Minimize assertions --- router/dataplane.go | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 7c28c21c6..8557016b1 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1648,18 +1648,9 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ unfold acc(p.d.Mem(), _) - // TODO[henri]: minimize assertions - // @ assert p.d.macFactory != nil - // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt)) // @ reveal p.d.DpAgreesWithSpec(dp) - // @ assert p.d.dpSpecWellConfiguredLocalIA(dp) - // @ assert dp.Asid() == io.AS{uint(p.d.localIA)} - // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} - // @ assert dp.Asid() == *p.d.asid - // @ assert p.macSpec.Asid() == *p.d.asid - // @ assert p.macSpec.Asid() == dp.Asid() v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP(/*@ dp @*/) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1671,17 +1662,9 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm) // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) - // TODO[henri]: minimize assertions // @ unfold acc(p.d.Mem(), _) - // @ assert p.d.macFactory != nil - // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} // @ reveal p.d.DpAgreesWithSpec(dp) // @ assert p.d.dpSpecWellConfiguredLocalIA(dp) - // @ assert dp.Asid() == io.AS{uint(p.d.localIA)} - // @ assert *p.d.asid == io.AS{uint(p.d.localIA)} - // @ assert dp.Asid() == *p.d.asid - // @ assert p.macSpec.Asid() == *p.d.asid - // @ assert p.macSpec.Asid() == dp.Asid() v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -2938,8 +2921,6 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/) - // TODO[henri]: might be able to remove this assertion - // @ assert p.macSpec.Asid() == old(p.macSpec.Asid()) // @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21) // @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21) if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 { From f7460a0564b7fbb0a7c2f52e8ca1aa914cab1853 Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 7 Oct 2025 01:31:29 +0200 Subject: [PATCH 20/22] Try to fix io-spec-lemmas.gobra --- router/io-spec-lemmas.gobra | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/router/io-spec-lemmas.gobra b/router/io-spec-lemmas.gobra index 81ffb39d1..7809dcfb6 100644 --- a/router/io-spec-lemmas.gobra +++ b/router/io-spec-lemmas.gobra @@ -274,6 +274,17 @@ func (p* scionPacketProcessor) AbsPktToSubSliceAbsPkt(ub []byte, start int, end assert reveal scion.validPktMetaHdr(ub[start:end]) unfold acc(p.scionLayer.Mem(ub), R56) reveal p.scionLayer.ValidHeaderOffset(ub, len(ub)) + // TODO: remove + assert scion.MetaLen <= len(ub) + metaHdr := scion.RawBytesToMetaHdr(ub[start:end]) + seg1 := int(metaHdr.SegLen[0]) + seg2 := int(metaHdr.SegLen[1]) + seg3 := int(metaHdr.SegLen[2]) + segs := io.CombineSegLens(seg1, seg2, seg3) + assert p.path.GetBase(ub[start:end]).PathMeta == metaHdr + assert p.path.GetBase(ub[start:end]).NumINF == segs.NumInfoFields() + assert p.path.GetBase(ub[start:end]).NumHops == segs.TotalHops() + assert p.path.GetBase(ub[start:end]) == scion.RawBytesToBase(ub[start:end]) assert p.path.GetBase(ub[start:end]).EqAbsHeader(ub[start:end]) fold acc(p.scionLayer.Mem(ub), R56) assert start == slayers.GetAddressOffset(ub) From e3e4f4e0982e110159bade035156c04e518cabc4 Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 7 Oct 2025 11:07:01 +0200 Subject: [PATCH 21/22] Simplify fix --- router/io-spec-lemmas.gobra | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/router/io-spec-lemmas.gobra b/router/io-spec-lemmas.gobra index 7809dcfb6..035a68caa 100644 --- a/router/io-spec-lemmas.gobra +++ b/router/io-spec-lemmas.gobra @@ -274,16 +274,6 @@ func (p* scionPacketProcessor) AbsPktToSubSliceAbsPkt(ub []byte, start int, end assert reveal scion.validPktMetaHdr(ub[start:end]) unfold acc(p.scionLayer.Mem(ub), R56) reveal p.scionLayer.ValidHeaderOffset(ub, len(ub)) - // TODO: remove - assert scion.MetaLen <= len(ub) - metaHdr := scion.RawBytesToMetaHdr(ub[start:end]) - seg1 := int(metaHdr.SegLen[0]) - seg2 := int(metaHdr.SegLen[1]) - seg3 := int(metaHdr.SegLen[2]) - segs := io.CombineSegLens(seg1, seg2, seg3) - assert p.path.GetBase(ub[start:end]).PathMeta == metaHdr - assert p.path.GetBase(ub[start:end]).NumINF == segs.NumInfoFields() - assert p.path.GetBase(ub[start:end]).NumHops == segs.TotalHops() assert p.path.GetBase(ub[start:end]) == scion.RawBytesToBase(ub[start:end]) assert p.path.GetBase(ub[start:end]).EqAbsHeader(ub[start:end]) fold acc(p.scionLayer.Mem(ub), R56) From 3aad84500bfae56b334d00d40fd014bd0947cc96 Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 7 Oct 2025 14:11:05 +0200 Subject: [PATCH 22/22] Adapt dataplane_spec_test --- router/dataplane_spec_test.gobra | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index 8af8b2618..bb0b374d0 100644 --- a/router/dataplane_spec_test.gobra +++ b/router/dataplane_spec_test.gobra @@ -12,8 +12,7 @@ // See the License for the specific language governing permissions and // limitations under the License. -// TODO: Include this file in the verification again. -// gobra +// +gobra package router @@ -86,12 +85,14 @@ requires macFactory != nil && len(*key) > 0 && acc(sl.Bytes(*key, 0, len(*key)), _) && scrypto.ValidKeyForHash(*key) && - macFactory implements MacFactorySpec{key} + acc(asid) && asid.V == 1000 && + macFactory implements MacFactorySpec{key, asid} requires metrics != nil && metrics.Mem() requires ctx != nil && ctx.Mem() func testRun( - macFactory func() hash.Hash, + macFactory func() (hash.Hash, ghost hash.ScionHashSpec), key *[]byte, + ghost asid gpointer[io.AS], metrics *Metrics, ctx context.Context, ghost place io.Place, @@ -130,6 +131,7 @@ func testRun( d.svc = newServices() d.macFactory = macFactory d.key = key + d.asid = asid d.localIA = 1000 d.Metrics = metrics d.bfdSessions = make(map[uint16]bfdSession)