From c0b039e6e0bee02dace5eb3a2865a5ffbd431f82 Mon Sep 17 00:00:00 2001 From: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com> Date: Wed, 15 Nov 2023 17:44:46 +0100 Subject: [PATCH] Concretize all abstract functions in the IO-spec (#231) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * making IO-spec dependend on abstract dataplane * renaming Abs_Dataplane to DataPlaneSpec * removing local state from IO-spec next place functions * rewriting IO-spec with match clause * comment out unnecessary functions * providing bodies to abstract functions in IO-spec * merge problems fix * cosmetic changes * IO-spec fix * adding receiving interface to topology * concretize dp3s_forward_ext * Apply suggestions from code review Co-authored-by: João Pereira * minor improvements * minor improvements * adding missing comment * renaming core and asid function * Update verification/io/io-spec.gobra * precondition for link_type function --------- Co-authored-by: João Pereira --- verification/io/dataplane_abstract.gobra | 51 +++++++++--- verification/io/io-spec.gobra | 99 ++++++++++++++++-------- verification/io/other_defs.gobra | 80 ++++++++++++------- verification/io/router.gobra | 84 ++++++++++++++++---- verification/io/router_events.gobra | 27 +++++-- verification/io/segment-defs.gobra | 16 ++-- verification/io/xover.gobra | 18 ++++- 7 files changed, 273 insertions(+), 102 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index f6fda5352..25b9af797 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -25,24 +25,36 @@ type DataPlaneSpec adt { } } -// TopologySpec provides information about the entire network topology. +// TopologySpec describes the entire network topology. // coreAS: IDs of the core Autonomous Systems // links: representation of the network topology as a graph. -// links[a1][1] == a2 means that AS a1 has an edge to AS a2 via interface 1. +// `links[(a1,x)] == (a2,y)` means that the interface x of AS a1 is connected +// to the interface y of AS a2. type TopologySpec adt { TopologySpec_{ coreAS set[IO_as] - links dict[IO_as](dict[IO_ifs]IO_as) + links dict[AsIfsPair]AsIfsPair } } +type AsIfsPair struct { + asid IO_as + ifs IO_ifs +} + ghost decreases -pure func (dp DataPlaneSpec) Valid() bool{ - return domain(dp.linkTypes) == domain(dp.neighborIAs) && - dp.localIA in domain(dp.topology.links) && - dp.neighborIAs == dp.topology.links[dp.localIA] && - (forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> core in domain(dp.topology.links)) +pure func (dp DataPlaneSpec) Valid() bool { + return domain(dp.linkTypes) == domain(dp.neighborIAs) && + (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} ifs in domain(dp.neighborIAs) ==> + (AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) && + dp.Lookup(AsIfsPair{dp.localIA, ifs}).asid == dp.neighborIAs[ifs])) && + (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) ==> + ifs in domain(dp.neighborIAs)) && + (forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.topology.links) ==> + let next_pair := dp.Lookup(pairs) in + (next_pair in domain(dp.topology.links)) && + dp.Lookup(next_pair) == pairs) } ghost @@ -52,6 +64,12 @@ pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link { return dp.linkTypes[ifs] } +ghost +decreases +pure func (dp DataPlaneSpec) GetNeighborIAs() dict[IO_ifs]IO_as { + return dp.neighborIAs +} + ghost requires ifs in domain(dp.neighborIAs) decreases @@ -61,12 +79,25 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as { ghost decreases -pure func (dp DataPlaneSpec) GetLocalIA() IO_as { +pure func (dp DataPlaneSpec) Asid() IO_as { return dp.localIA } ghost decreases -pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] { +pure func (dp DataPlaneSpec) Core() set[IO_as] { return dp.topology.coreAS } + +ghost +decreases +pure func (dp DataPlaneSpec) GetLinks() dict[AsIfsPair]AsIfsPair { + return dp.topology.links +} + +ghost +requires pair in domain(dp.topology.links) +decreases +pure func(dp DataPlaneSpec) Lookup(pair AsIfsPair) AsIfsPair { + return dp.topology.links[pair] +} \ No newline at end of file diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 652c59a1c..07a8af20d 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -18,6 +18,10 @@ package io +// Unlike the original IO-spec from Isabelle, we need additional information about the network topology. +// To ensure the well-formedness of all map accesses we require an additional conjunction +// for all the events (dp.Valid()) + // This is the main IO Specification. pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { dp.dp3s_iospec_bio3s_enter(s, t) && @@ -45,13 +49,14 @@ requires CBio_IN_bio3s_enter(t, v) decreases pure func CBio_IN_bio3s_enter_T(t Place, v IO_val) Place - +/*** Helper functions, not in Isabelle ***/ +// Establishes the traversed segment for packets which are not incremented (internal). ghost requires len(currseg.Future) > 0 decreases -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { +pure func establishGuardTraversedseg(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? - dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : + upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in IO_seg3_ { AInfo: currseg.AInfo, @@ -63,22 +68,47 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg History: currseg.History} } +// Establishes the traversed segment for packets that are incremented (external). +ghost +requires len(currseg.Future) > 0 +decreases +pure func establishGuardTraversedsegInc(currseg IO_seg3) IO_seg3 { + return let uinfo := !currseg.ConsDir ? + upd_uinfo(currseg.UInfo, currseg.Future[0]) : + currseg.UInfo in + IO_seg3_ { + AInfo: currseg.AInfo, + UInfo: uinfo, + ConsDir: currseg.ConsDir, + Peer: currseg.Peer, + Past: seq[IO_HF]{currseg.Future[0]} ++ currseg.Past, + Future: currseg.Future[1:], + History: seq[IO_ahi]{currseg.Future[0].Toab()} ++ currseg.History} +} +/*** End of helper functions, not in Isabelle ***/ + // This corresponds to the condition of the if statement in the io-spec case for enter ghost requires v.isIO_Internal_val1 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return some(v.IO_Internal_val1_2) in domain(s.ibuf) ==> + return some(v.IO_Internal_val1_2) in domain(s.ibuf) && (let ibuf_set := s.ibuf[some(v.IO_Internal_val1_2)] in (v.IO_Internal_val1_1 in ibuf_set)) && len(v.IO_Internal_val1_1.CurrSeg.Future) > 0 && let currseg := v.IO_Internal_val1_1.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in - let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in + let traversedseg := match v.IO_Internal_val1_4{ + case none[IO_ifs]: + establishGuardTraversedseg(currseg) + default: + establishGuardTraversedsegInc(currseg) + } in dp.dp2_enter_guard( v.IO_Internal_val1_1, currseg, traversedseg, - dp.asid(), + dp.Asid(), hf1, v.IO_Internal_val1_2, fut) && @@ -98,12 +128,13 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) forall v IO_val :: { dp.dp3s_iospec_bio3s_enter_guard(s, t, v) } ( match v { case IO_Internal_val1{_, _, ?newpkt, ?nextif}: - (dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> + (dp.Valid() && dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> (CBio_IN_bio3s_enter(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_add_obuf(s, nextif, newpkt), CBio_IN_bio3s_enter_T(t, v)))) - default: true + default: + true }) } @@ -116,6 +147,7 @@ pure func dp3s_iospec_bio3s_xover_up2down_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for xover_up2down ghost requires v.isIO_Internal_val1 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { return let currseg := v.IO_Internal_val1_1.CurrSeg in @@ -127,9 +159,10 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta (nextseg.ConsDir && len(nextseg.Future) > 0 && len(currseg.Future) > 0 && + len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in - (dp.xover_up2down2_link_type(dp.asid(), hf1, hf2) && + let traversedseg := establishGuardTraversedsegInc(currseg) in + (dp.xover_up2down2_link_type(dp.Asid(), hf1, hf2) && dp.dp3s_xover_common( s, v.IO_Internal_val1_1, @@ -146,14 +179,14 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta } pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) }{ CBio_IN_bio3s_xover_up2down(t, v) } { dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_up2down_T(t, v)) } ( + forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) }{ CBio_IN_bio3s_xover_up2down(t, v) } { dp.dp3s_iospec_ordered(dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_up2down_T(t, v)) } ( match v { case IO_Internal_val1{_, _, ?newpkt, ?nextif}: - (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> + (dp.Valid() && dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> (CBio_IN_bio3s_xover_up2down(t, v) && - dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), - dp3s_iospec_bio3s_xover_up2down_T(t, v)))) + dp.dp3s_iospec_ordered( + dp3s_add_obuf(s, nextif, newpkt), + dp3s_iospec_bio3s_xover_up2down_T(t, v)))) default: true }) @@ -167,10 +200,11 @@ pure func dp3s_iospec_bio3s_xover_core_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for xover_core ghost -decreases requires v.isIO_Internal_val1 +requires dp.Valid() +decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return (dp.asid() in dp.core() && + return (dp.Asid() in dp.Core() && let currseg := v.IO_Internal_val1_1.CurrSeg in match v.IO_Internal_val1_1.LeftSeg { case none[IO_seg2]: @@ -180,9 +214,10 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ currseg.ConsDir == nextseg.ConsDir && len(nextseg.Future) > 0 && len(currseg.Future) > 0 && + len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in - (dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && + let traversedseg := establishGuardTraversedsegInc(currseg) in + (dp.xover_core2_link_type(hf1, hf2, dp.Asid(), currseg.ConsDir) && dp.dp3s_xover_common( s, v.IO_Internal_val1_1, @@ -199,20 +234,19 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ } pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) }{ CBio_IN_bio3s_xover_core(t, v) }{ dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_core_T(t, v)) } ( + forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) }{ CBio_IN_bio3s_xover_core(t, v) }{ dp.dp3s_iospec_ordered(dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_core_T(t, v)) } ( match v { case IO_Internal_val1{_, _, ?newpkt, ?nextif}: - (dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> + (dp.Valid() && dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> (CBio_IN_bio3s_xover_core(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_add_obuf(s, nextif, newpkt), dp3s_iospec_bio3s_xover_core_T(t, v)))) default: true }) } - pred CBio_IN_bio3s_exit(t Place, v IO_val) ghost @@ -222,21 +256,23 @@ pure func dp3s_iospec_bio3s_exit_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for exit ghost requires v.isIO_Internal_val2 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return none[IO_ifs] in domain(s.ibuf) ==> + return none[IO_ifs] in domain(s.ibuf) && (let ibuf_set := s.ibuf[none[IO_ifs]] in (v.IO_Internal_val2_1 in ibuf_set)) && + len(v.IO_Internal_val2_1.CurrSeg.Future) > 0 && dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3) } pred (dp DataPlaneSpec) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ CBio_IN_bio3s_exit(t, v) }{ dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2), dp3s_iospec_bio3s_exit_T(t, v)) } ( + forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ CBio_IN_bio3s_exit(t, v) }{ dp.dp3s_iospec_ordered(dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2), dp3s_iospec_bio3s_exit_T(t, v)) } ( match v { case IO_Internal_val2{_, ?newpkt, ?nextif}: - (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> + (dp.Valid() && dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> (CBio_IN_bio3s_exit(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, some(nextif), newpkt), + dp3s_add_obuf(s, some(nextif), newpkt), dp3s_iospec_bio3s_exit_T(t, v)))) default: true @@ -253,9 +289,10 @@ pure func dp3s_iospec_bio3s_send_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for send ghost requires v.isIO_val_Pkt2 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return v.IO_val_Pkt2_1 in domain(s.obuf) ==> + return v.IO_val_Pkt2_1 in domain(s.obuf) && (let obuf_set := s.obuf[v.IO_val_Pkt2_1] in (v.IO_val_Pkt2_2 in obuf_set)) } @@ -264,7 +301,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { forall v IO_val :: { dp.dp3s_iospec_bio3s_send_guard(s, t, v) }{ CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v)) }{ CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v)) } ( match v { case IO_val_Pkt2{_, _}: - (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> + (dp.Valid() && dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> CBioIO_bio3s_send(t, v) && dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v))) case IO_val_Unsupported{_, _}: @@ -290,7 +327,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { (match dp3s_iospec_bio3s_recv_R(t) { case IO_val_Pkt2{?recvif, ?pkt}: dp.dp3s_iospec_ordered( - dp.dp3s_add_ibuf(s, recvif, pkt), dp3s_iospec_bio3s_recv_T(t)) + dp3s_add_ibuf(s, recvif, pkt), dp3s_iospec_bio3s_recv_T(t)) case IO_val_Unsupported{_, _}: dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_recv_T(t)) default: diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index 126361f5c..807dd9ee7 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -34,9 +34,6 @@ type IO_ifs uint16 // type of AS identifiers type IO_as uint -// router ids -type IO_rid uint - // msgTerms consist of terms from our term algebra. type IO_msgterm adt { MsgTerm_Empty{} @@ -46,7 +43,7 @@ type IO_msgterm adt { } MsgTerm_Num { - MsgTerm_Num_ int // formallized as nat in Isabelle + MsgTerm_Num_ uint // formallized as nat in Isabelle } MsgTerm_Key { @@ -58,7 +55,7 @@ type IO_msgterm adt { } MsgTerm_FS { - MsgTerm_FS_ seq[IO_msgterm] + MsgTerm_FS_ set[IO_msgterm] } MsgTerm_MPair { @@ -122,49 +119,79 @@ type IO_Link adt { IO_PeerOrCore{} IO_NoLink{} } -/* End of Link Types */ - -/* To clarify, the existence of the following functions seems to be assumed */ -// NOTE: -// The following functions are provided as parameters to various locales in the Isabelle formalization. -// However, it is not clear at the moment how these should be translated to Gobra and whether they -// should have proof obligations attached, or can just be assumed to exist. +// This function is provided as locale in the Isabelle formalization. +// This function is only ever called with p1 == dp.Asid(). As a future optimization +// this parameter and precondition can be dropped. ghost +requires dp.Valid() +requires p1 == dp.Asid() decreases -pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as +pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ + return p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} +} ghost +requires dp.Valid() +requires asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link +pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{ + return dp.egif2_type(hf1, asid, IO_Link(IO_CustProv{})) +} -ghost -decreases -pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool ghost +requires dp.Valid() +requires asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool{ + return dp.egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) +} ghost +requires dp.Valid() +requires asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool{ + return dp.egif2_type(hf1, asid, IO_Link(IO_ProvCust{})) +} ghost +requires dp.Valid() +requires asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool{ + return dp.inif2_type(hf1, asid, IO_Link(IO_ProvCust{})) +} ghost +requires dp.Valid() +requires asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool{ + return dp.inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) +} ghost +requires dp.Valid() +requires asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool{ + return dp.inif2_type(hf1, asid, IO_Link(IO_CustProv{})) +} ghost +requires dp.Valid() +requires ifs != none[IO_ifs] ==> asid == dp.Asid() decreases -pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool +pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{ + return match ifs { + case none[IO_ifs]: + false + default: + dp.link_type(asid, get(ifs)) == link + } +} type ext2_rec struct { op1 IO_as @@ -182,9 +209,8 @@ type IO_dp2_state adt { } } -// extract_asid ghost decreases -pure func (m IO_msgterm) extract_asid() IO_as - -/* End of To clarify */ \ No newline at end of file +pure func (m IO_msgterm) extract_asid() IO_as { + return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_ +} diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 3370e716a..6be780804 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -20,36 +20,82 @@ package io // TODO: make individual_router an interface type with the following methods -// This function corresponds to function 'core' in the IO spec +ghost +decreases +pure func if2term(ifs option[IO_ifs]) IO_msgterm { + return match ifs { + case none[IO_ifs]: + MsgTerm_Empty{} + default: + IO_msgterm(MsgTerm_AS{IO_as(get(ifs))}) + } +} + ghost decreases -pure func (dp DataPlaneSpec) core() set[IO_as] +pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool { + return let inif := hf.InIF2 in + let egif := hf.EgIF2 in + let x := hf.HVF in + let l := IO_msgterm(MsgTerm_L{ + seq[IO_msgterm]{ + IO_msgterm(MsgTerm_Num{ts}), + if2term(inif), + if2term(egif), + IO_msgterm(MsgTerm_FS{uinfo})}}) in + x == mac(macKey(asidToKey(dp.Asid())), l) +} ghost decreases -pure func (dp DataPlaneSpec) hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool +pure func macKey(key IO_key) IO_msgterm { + return IO_msgterm(MsgTerm_Key{key}) +} +ghost +decreases +pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm { + return IO_msgterm( MsgTerm_Hash { + MsgTerm_Hash_ : IO_msgterm( MsgTerm_MPair{ + MsgTerm_MPair_1 : fst, + MsgTerm_MPair_2 : snd, + }), + }) +} + +// helper function, not defined in IO spec ghost decreases -pure func (dp DataPlaneSpec) upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] +pure func asidToKey(asid IO_as) IO_key{ + return IO_key(Key_macK{asid}) +} ghost decreases -pure func (dp DataPlaneSpec) rid() IO_rid +pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{ + return let setHVF := set[IO_msgterm]{hf.HVF} in + (segid union setHVF) setminus (segid intersection setHVF) +} ghost decreases pure func (dp DataPlaneSpec) asid() IO_as { - return dp.rid_as(dp.rid()) + return dp.Asid() } + +// This function is provided as locale in the Isabelle formalization. ghost +requires dp.Valid() decreases -pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool +pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool { + return AsIfsPair{asid, nextif} in domain(dp.GetLinks()) && + dp.Lookup(AsIfsPair{asid, nextif}) == AsIfsPair{a2, i2} +} ghost decreases -pure func (dp DataPlaneSpec) dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { +pure func dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { return IO_dp3s_state_local_{ ibuf: insert(s.ibuf, i, pkt), obuf: s.obuf, @@ -58,7 +104,7 @@ pure func (dp DataPlaneSpec) dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_if ghost decreases -pure func (dp DataPlaneSpec) dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { +pure func dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { return IO_dp3s_state_local_{ ibuf: s.ibuf, obuf: insert(s.obuf, i, pkt), @@ -69,20 +115,28 @@ pure func (dp DataPlaneSpec) dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_if ghost decreases pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { - return let newSet := (k in domain(buf)? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in + return let newSet := (k in domain(buf) ? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in buf[k = newSet] } -// TODO: try to remove the existencials here ghost +requires len(m.CurrSeg.Future) > 0 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { - return (exists currseg IO_seg3, traversedseg IO_seg3, fut seq[IO_HF], hf1 IO_HF :: { dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) } dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1)) && - (exists a2 IO_as, i2 IO_ifs :: { dp.is_target(dp.asid(), nextif, a2, i2) } dp.is_target(dp.asid(), nextif, a2, i2)) + return let currseg := m.CurrSeg in + let hf1, fut := currseg.Future[0], currseg.Future[1:] in + let traversedseg := establishGuardTraversedsegInc(currseg) in + dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && + let a2 := dp.GetNeighborIA(nextif) in + let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in + dp.is_target(dp.Asid(), nextif, a2, i2) } // TODO: should we change IO_ifs to being implemented as an option type? ghost +requires len(m.CurrSeg.Future) > 0 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { return match nextif { @@ -94,6 +148,8 @@ pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif opti } ghost +requires len(intermediatepkt.CurrSeg.Future) > 0 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_xover_common( s IO_dp3s_state_local, @@ -112,6 +168,6 @@ pure func (dp DataPlaneSpec) dp3s_xover_common( // this is because of the way math. maps are implemented, we can only obtain a key that is in the map before. return some(recvif) in domain(s.ibuf) && (let lookupRes := s.ibuf[some(recvif)] in (m in lookupRes)) && - dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, hf1.extr_asid(), recvif) && + dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, dp.Asid(), recvif) && dp.dp3s_forward(intermediatepkt, newpkt, nextif) } diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index ea64ce2b7..3159fa1dc 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -19,6 +19,8 @@ package io ghost +requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool { return d? @@ -28,6 +30,8 @@ pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) /* Abbreviations */ ghost +requires dp.Valid() +requires a == dp.Asid() decreases pure func (dp DataPlaneSpec) valid_link_types2(hf1 IO_HF, a IO_as) bool { return (dp.egif_prov2(hf1, a) && dp.inif_cust2(hf1, a)) || @@ -36,6 +40,8 @@ pure func (dp DataPlaneSpec) valid_link_types2(hf1 IO_HF, a IO_as) bool { } ghost +requires dp.Valid() +requires a == dp.Asid() decreases pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool { return (dp.inif_prov2(hf1, a) && dp.egif_cust2(hf1, a)) || @@ -45,6 +51,8 @@ pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool { /* End of Abbreviations */ ghost +requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool { return (d && hf1.InIF2 === some(recvif) && dp.valid_link_types_in2(hf1, asid)) || @@ -53,40 +61,43 @@ pure func (dp DataPlaneSpec) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, ghost decreases -pure func (dp DataPlaneSpec) dp2_exit_interface(d bool, asid IO_as, hf1 IO_HF, outif IO_ifs) bool { +pure func dp2_exit_interface(d bool, asid IO_as, hf1 IO_HF, outif IO_ifs) bool { return (d && hf1.EgIF2 == some(outif)) || (!d && hf1.InIF2 == some(outif)) } // Takes a packet and forwards it externally, incrementing the segment before doing so. ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif IO_ifs, currseg, traversedseg IO_seg2, newpkt IO_pkt2, fut seq[IO_HF], hf1 IO_HF) bool { return m.CurrSeg == currseg && newpkt == IO_pkt2(IO_Packet2{traversedseg, m.LeftSeg, m.MidSeg, m.RightSeg}) && // The outgoing interface is correct: - dp.dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) && + dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) && // Next validate the current hop field with the *original* UInfo field): dp.hf_valid(currseg.ConsDir, currseg.AInfo, currseg.UInfo, hf1) && hf1.extr_asid() == asid && // Segment update: push current hop field into the Past path and History: - dp.inc_seg2(currseg, traversedseg, hf1, fut) && + inc_seg2(currseg, traversedseg, hf1, fut) && // If the current segment is an *down*-segment, then we need to update the // uinfo field *after* validating the hop field - dp.update_uinfo(currseg.ConsDir, currseg, traversedseg, hf1) && + update_uinfo(currseg.ConsDir, currseg, traversedseg, hf1) && // Other fields: no update - dp.same_other2(currseg, traversedseg) + same_other2(currseg, traversedseg) } // A packet is received from an ext state (i.e., an inter-AS channel) and is forwarded (either internally or externally) ghost +requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_enter_guard(m IO_pkt2, currseg IO_seg2, traversedseg IO_seg2, asid IO_as, hf1 IO_HF, recvif IO_ifs, fut seq[IO_HF]) bool { return m.CurrSeg == currseg && currseg.Future == seq[IO_HF]{hf1} ++ fut && dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && - dp.update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && - dp.same_segment2(currseg, traversedseg) && - dp.same_other2(currseg, traversedseg) && + update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && + same_segment2(currseg, traversedseg) && + same_other2(currseg, traversedseg) && dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && hf1.extr_asid() == asid } diff --git a/verification/io/segment-defs.gobra b/verification/io/segment-defs.gobra index a89feca0a..5349fe31b 100644 --- a/verification/io/segment-defs.gobra +++ b/verification/io/segment-defs.gobra @@ -23,7 +23,7 @@ package io ghost decreases -pure func (dp DataPlaneSpec) inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, fut seq[IO_HF]) bool { +pure func inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, fut seq[IO_HF]) bool { return currseg.Future === seq[IO_HF]{hf1} ++ fut && traversedseg.Future === fut && traversedseg.Past === seq[IO_HF]{hf1} ++ currseg.Past && @@ -32,7 +32,7 @@ pure func (dp DataPlaneSpec) inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, ghost decreases -pure func (dp DataPlaneSpec) same_segment2(currseg, traversedseg IO_seg2) bool { +pure func same_segment2(currseg, traversedseg IO_seg2) bool { return traversedseg.Future === currseg.Future && traversedseg.Past === currseg.Past && traversedseg.History === currseg.History @@ -40,25 +40,25 @@ pure func (dp DataPlaneSpec) same_segment2(currseg, traversedseg IO_seg2) bool { ghost decreases -pure func (dp DataPlaneSpec) update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { - return traversedseg.UInfo === dp.upd_uinfo(currseg.UInfo, hf1) +pure func update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { + return traversedseg.UInfo === upd_uinfo(currseg.UInfo, hf1) } ghost decreases -pure func (dp DataPlaneSpec) same_uinfo2(currseg, traversedseg IO_seg2) bool { +pure func same_uinfo2(currseg, traversedseg IO_seg2) bool { return currseg.UInfo === traversedseg.UInfo } ghost decreases -pure func (dp DataPlaneSpec) update_uinfo(condition bool, currseg, traversedseg IO_seg2, hf1 IO_HF) bool { - return condition? dp.update_uinfo2(currseg, traversedseg, hf1) : dp.same_uinfo2(currseg, traversedseg) +pure func update_uinfo(condition bool, currseg, traversedseg IO_seg2, hf1 IO_HF) bool { + return condition? update_uinfo2(currseg, traversedseg, hf1) : same_uinfo2(currseg, traversedseg) } ghost decreases -pure func (dp DataPlaneSpec) same_other2(currseg, traversedseg IO_seg3) bool { +pure func same_other2(currseg, traversedseg IO_seg3) bool { return traversedseg.AInfo === currseg.AInfo && traversedseg.ConsDir === currseg.ConsDir && traversedseg.Peer === currseg.Peer diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra index 82a95c0ee..e9cda55ad 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -35,6 +35,8 @@ package io // remaining hop field into the Past path, and nextseg, which is // the new segment that we are xovering over to. ghost +requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, currseg IO_seg2, @@ -54,28 +56,34 @@ pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, nextseg.Future[0] == hf2 && dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && dp.dp2_check_recvif(currseg.ConsDir, asid, recvif) && - dp.update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && - dp.inc_seg2(currseg, traversedseg, hf1, seq[IO_HF]{}) && + update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && + inc_seg2(currseg, traversedseg, hf1, seq[IO_HF]{}) && dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && dp.hf_valid(nextseg.ConsDir, nextseg.AInfo, nextseg.UInfo, hf2) && hf1.extr_asid() == asid && hf2.extr_asid() == asid && - dp.same_other2(currseg, traversedseg) + same_other2(currseg, traversedseg) } ghost +requires dp.Valid() +requires a == dp.Asid() decreases pure func (dp DataPlaneSpec) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { return dp.if_type(a, hf.EgIF2, link) } ghost +requires dp.Valid() +requires a == dp.Asid() decreases pure func (dp DataPlaneSpec) inif2_type(hf IO_HF, a IO_as, link IO_Link) bool { return dp.if_type(a, hf.InIF2, link) } ghost +requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 IO_HF) bool { return (dp.egif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) || @@ -84,8 +92,10 @@ pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 } ghost +requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) xover_core2_link_type(hf1 IO_HF, hf2 IO_HF, asid IO_as, d bool) bool { return (!d && dp.egif2_type(hf1, asid, IO_ProvCust{}) && dp.inif2_type(hf2, asid, IO_PeerOrCore{})) || (d && dp.inif2_type(hf1, asid, IO_PeerOrCore{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) -} \ No newline at end of file +}