[WIP] SIF

pkg/slayers/scion_spec.gobra

@@ -412,20 +412,21 @@ requires acc(sl.Bytes(ub, 0, len(ub)), _)
 decreases
 func (s *SCION) EqAbsHeader(ub []byte) bool {
 	return unfolding acc(s.Mem(ub), _) in
-		let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in
+		// SIF: rename due to conflict with low assertion
+		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 acc(s.Path.Mem(ub[low:high]), _) in
+		unfolding acc(s.Path.Mem(ub[low_:high]), _) in
 		unfolding acc(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
@@ -442,10 +443,11 @@ requires acc(s.Mem(ub), _)
 decreases
 func (s *SCION) ValidScionInitSpec(ub []byte) bool {
 	return unfolding acc(s.Mem(ub), _)                  in
-		let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in
+		// SIF: rename due to conflict with low assertion
+		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.

router/dataplane.go

@@ -145,12 +145,21 @@ type BatchConn interface {
 	// @ ensures   err == nil ==>
 	// @ 	forall i int :: { &msgs[i] } 0 <= i && i < n ==>
 	// @ 		MsgToAbsVal(&msgs[i], ingressID) == old(MultiReadBioIO_val(place, n)[i])
+	// SIF: classification spec
+	// NOTE: The postcondition for recv specifies that received messages are low.
+	// TODO: I have decided to mark the abstraction as low for now.
+	// And also used MultiReadBioIOI_val instead of MsgToAbsVal to match what is
+	// used in permissions.
+	// @ ensures err == nil ==>
+	// @ 	forall i int :: { MutliReadBioIO_val(place, n)[i] } 0 <= i && i < n ==>
+	// @		low(old(MultiReadBioIO_val(place, n)[i]))
 	ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place @*/) (n int, err error)
 	// @ requires  acc(addr.Mem(), _)
 	// @ requires  acc(Mem(), _)
 	// @ preserves acc(sl.Bytes(b, 0, len(b)), R10)
 	// @ ensures   err == nil ==> 0 <= n && n <= len(b)
 	// @ ensures   err != nil ==> err.ErrorMem()
+	// SIF: add to classification spec later as well (bfdSend)
 	WriteTo(b []byte, addr *net.UDPAddr) (n int, err error)
 	// @ requires  acc(Mem(), _)
 	// (VerifiedSCION) opted for less reusable spec for WriteBatch for
@@ -161,6 +170,10 @@ type BatchConn interface {
 	// preconditions for IO-spec:
 	// @ requires  MsgToAbsVal(&msgs[0], egressID) == ioAbsPkts
 	// @ requires  io.token(place) && io.CBioIO_bio3s_send(place, ioAbsPkts)
+	// SIF: classification spec
+	// NOTE: I mark `ioAbsPkts` instead of `MsgToAbsVal(...)` as low here to
+	// match variable used in send permission.
+	// @ requires low(ioAbsPkts)
 	// @ ensures   acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr()
 	// @ ensures   acc(sl.Bytes(msgs[0].GetFstBuffer(), 0, len(msgs[0].GetFstBuffer())), R50)
 	// @ ensures   err == nil ==> 0 <= n && n <= len(msgs)

router/io-spec-atomic-events.gobra

@@ -155,6 +155,36 @@ func AtomicXover(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pk
 	UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt)
 	ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt)
 	ghost *ioSharedArg.Place = tN
+	fold SharedInv!< dp, ioSharedArg !>()
+	ghost ioLock.Unlock()
+}
+
+ghost
+// NOTE: I don't think I need this here
+// requires dp.Valid()
+requires low(beta) && low(ts) && low(inif) && low(egif)
+requires sigma == io.nextMsgtermSpec(dp.Asid(), inif, egif, ts, beta)
+preserves acc(ioLock.LockP(), _)
+preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
+ensures low(sigma)
+// NOTE: Seems to be needed bc. lock might not terminate
+decreases _
+func AtomicDecl(beta set[io.IO_msgterm], ts uint, inif, egif option[io.IO_ifs], sigma io.IO_msgterm, ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+	ghost ioLock.Lock()
+	unfold SharedInv!< dp, ioSharedArg !>()
+
+	t, s := *ioSharedArg.Place, *ioSharedArg.State
+	ghost tag := io.IO_val(io.IO_decl_val{beta, ts, inif, egif, sigma})
+
+	assert dp.dp4s_iospec_bio4s_decl_guard(s, t, tag)
+	unfold dp.dp3s_iospec_ordered(s, t)
+	unfold dp.dp4s_iospec_bio4s_decl(s, t)
+
+	io.TriggerBodyIoDecl(tag)
+	tN := io.dp4s_iospec_bio4s_decl_T(t, tag)
+	io.Decl(t, tag)
+	ghost *ioSharedArg.Place = tN
+
 	fold SharedInv!< dp, ioSharedArg !>()
 	ghost ioLock.Unlock()
 }

verification/io/io-spec.gobra

@@ -33,7 +33,9 @@ pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) {
 	dp.dp3s_iospec_bio3s_send(s, t) &&
 	dp.dp3s_iospec_bio3s_recv(s, t) &&
 	dp.dp3s_iospec_skip(s, t) &&
-	dp.dp3s_iospec_stop(s, t)
+	dp.dp3s_iospec_stop(s, t) &&
+	// SIF:
+	dp.dp4s_iospec_bio4s_decl(s, t)
 }
 
 type Place int
@@ -299,6 +301,55 @@ pred (dp DataPlaneSpec) dp3s_iospec_stop(s IO_dp3s_state_local, t Place) {
 	true
 }
 
+/* SIF: Declassification specification.
+I use "4s" to distinguish additions of the refined event system. */
+pred CBio_IN_bio4s_decl(t Place, v IO_val)
+
+// SIF: Return next place
+ghost 
+// SIF: I left out `requires CBio_IN_bio4s_decl(t, v)` as we deem it not necessary.
+decreases
+pure func dp4s_iospec_bio4s_decl_T(t Place, v IO_val) Place
+
+ghost
+requires v.isIO_decl_val
+// NOTE: Not sure I need this here
+// requires dp.Valid()
+decreases
+pure func (dp DataPlaneSpec) dp4s_iospec_bio4s_decl_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+	// SIF: cf. `hf_valid` in `router.gobra`
+	// NOTE: For some reason, formatting this differently leads to a parsing error.
+	return v.IO_decl_val_sigma == (nextMsgtermSpec(
+		dp.Asid(), 
+		v.IO_decl_val_inif, 
+		v.IO_decl_val_egif, 
+		v.IO_decl_val_ts, 
+		v.IO_decl_val_beta))
+}
+
+pred (dp DataPlaneSpec) dp4s_iospec_bio4s_decl(s IO_dp3s_state_local, t Place) {
+	// SIF: just copying with `TriggerBodyIoEnter` for now.
+	// NOTE: here as well we need some specific formatting
+	forall v IO_val :: { TriggerBodyIoDecl(v) } (
+		match v {
+			case IO_decl_val{?beta, ?ts, ?inif, ?egif, ?sigma}:
+				let _ignored := TriggerBodyIoDecl(v) in
+				// NOTE: Not sure I need this here
+				// (dp.Valid() && dp.dp4s_iospec_bio4s_decl_guard(s, t, v) ==>
+				(dp.dp4s_iospec_bio4s_decl_guard(s, t, v) ==>
+					(CBio_IN_bio4s_decl(t, v) &&
+					dp.dp3s_iospec_ordered(
+						s, 
+						dp4s_iospec_bio4s_decl_T(t, v))))
+			default:
+				true
+		})
+}
+
+ghost
+decreases
+pure func TriggerBodyIoDecl(v IO_val) BogusTrigger { return BogusTrigger{} }
+
 /** BIO operations **/
 ghost
 decreases
@@ -318,4 +369,14 @@ requires token(t) && CBio_IN_bio3s_exit(t, v)
 ensures  token(old(dp3s_iospec_bio3s_exit_T(t, v)))
 func Exit(ghost t Place, ghost v IO_val)
 
+// SIF: declassification action
+// TODO: maybe it's a good idea to split up sigma and p in IO_val
+ghost
+decreases
+requires token(t) && CBio_IN_bio4s_decl(t, v)
+requires v.isIO_decl_val && low(v.IO_decl_val_inif) && low(v.IO_decl_val_egif) && low(v.IO_decl_val_ts) && low(v.IO_decl_val_beta)
+ensures token(dp4s_iospec_bio4s_decl_T(t, v))
+ensures low(v.IO_decl_val_sigma)
+func Decl(ghost t Place, ghost v IO_val)
+
 /** End of helper functions to perfrom BIO operations **/

verification/io/values.gobra

@@ -52,4 +52,17 @@ type IO_val adt {
 		IO_Internal_val2_2 IO_pkt3
 		IO_Internal_val2_3 IO_ifs
 	}
+
+	/* SIF: Output (to env.) for declassification action.
+	This consists of the segment identifier `beta`, the timestamp `ts, the 
+	ingress and egress interfaces `inif` and `egif` (resp.), and a hop 
+	authenticator `sigma`. 
+	Also see `router.gobra` for  types. */
+	IO_decl_val {
+		IO_decl_val_beta set[IO_msgterm]  // uinfo
+		IO_decl_val_ts uint
+		IO_decl_val_inif option[IO_ifs]
+		IO_decl_val_egif option[IO_ifs]
+		IO_decl_val_sigma IO_msgterm
+	}
 }