From d61970f81c9c94cf3ebbeea55f17f7966269b253 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 24 Jul 2024 15:27:28 +0200 Subject: [PATCH 1/7] make hf_valid opaque --- verification/io/router.gobra | 1 + 1 file changed, 1 insertion(+) diff --git a/verification/io/router.gobra b/verification/io/router.gobra index f1741bed5..5531a8d4b 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -33,6 +33,7 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm { ghost decreases +opaque 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 From 82b08bc83ff6880561e1a0fcfa325ac99796bbd4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Jul 2024 00:58:51 +0200 Subject: [PATCH 2/7] backup --- router/io-spec-abstract-transitions.gobra | 1 + .../github.com/google/gopacket/base.gobra | 4 +- verification/io/dataplane_abstract.gobra | 12 +++--- verification/io/router.gobra | 39 +++++++++++++++---- 4 files changed, 40 insertions(+), 16 deletions(-) diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index 8aa346ff3..083e01089 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -205,6 +205,7 @@ func ExternalEnterOrExitEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], ne reveal AbsValidateEgressIDConstraint(nextPkt, (ingressID != none[io.IO_ifs]), dp) reveal AbsProcessEgress(nextPkt) if(ingressID == none[io.IO_ifs]){ + // assert false AtomicExit(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) } else { AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra index 6a55f340e..9c0ae5c81 100644 --- a/verification/dependencies/github.com/google/gopacket/base.gobra +++ b/verification/dependencies/github.com/google/gopacket/base.gobra @@ -60,8 +60,8 @@ ensures len(res) != 0 ==> res === ub[start:end] decreases func (p Payload) Payload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { res = []byte(p) - assert unfolding acc(p.Mem(ub), R20) in true - return res, 0, len(p) + assert unfolding acc(p.Mem(ub), R20) in true + return res, 0, len(p) } requires b != nil && b.Mem() diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index ba717326a..e78c901e9 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -21,16 +21,16 @@ package io // to the interface y of AS a2. type DataPlaneSpec adt { DataPlaneSpec_{ - linkTypes dict[IO_ifs]IO_Link - neighborIAs dict[IO_ifs]IO_as - localIA IO_as - links dict[AsIfsPair]AsIfsPair + linkTypes dict[IO_ifs]IO_Link + neighborIAs dict[IO_ifs]IO_as + localIA IO_as + links dict[AsIfsPair]AsIfsPair } } type AsIfsPair struct { - asid IO_as - ifs IO_ifs + asid IO_as + ifs IO_ifs } ghost diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 5531a8d4b..6541d36bc 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -33,20 +33,43 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm { ghost decreases -opaque 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) + let next := dp.nextMsgtermSpec(inif, egif, ts, uinfo) in + x == next +} + +ghost +//opaque +decreases +pure func (dp DataPlaneSpec) nextMsgtermSpec(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm { + // return let l := MsgTerm_L { + // seq[IO_msgterm]{ + // MsgTerm_Num{ts}, + // if2term(inif), + // if2term(egif), + // MsgTerm_FS{uinfo}}, + // } in mac(macKey(asidToKey(dp.Asid())), l) + return let l := plaintextToMac(inif, egif, ts, uinfo) in + mac(macKey(asidToKey(dp.Asid())), l) +} + +ghost +opaque +decreases +pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm { + return MsgTerm_L { + seq[IO_msgterm]{ + MsgTerm_Num{ts}, + if2term(inif), + if2term(egif), + MsgTerm_FS{uinfo}}, + } } + ghost decreases pure func macKey(key IO_key) IO_msgterm { From 5bd3b1e6ab374ea14657dfec3cc93954f38293cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Jul 2024 01:07:32 +0200 Subject: [PATCH 3/7] backup --- verification/io/router.gobra | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 6541d36bc..685d04810 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -27,7 +27,7 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm { case none[IO_ifs]: MsgTerm_Empty{} default: - IO_msgterm(MsgTerm_AS{IO_as(get(ifs))}) + MsgTerm_AS{IO_as(get(ifs))} } } @@ -65,33 +65,33 @@ pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinf MsgTerm_Num{ts}, if2term(inif), if2term(egif), - MsgTerm_FS{uinfo}}, + MsgTerm_FS{uinfo}, + }, } } - ghost decreases pure func macKey(key IO_key) IO_msgterm { - return IO_msgterm(MsgTerm_Key{key}) + return 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, - }), - }) + return MsgTerm_Hash { + MsgTerm_Hash_: MsgTerm_MPair { + MsgTerm_MPair_1: fst, + MsgTerm_MPair_2: snd, + }, + } } // helper function, not defined in IO spec ghost decreases -pure func asidToKey(asid IO_as) IO_key{ - return IO_key(Key_macK{asid}) +pure func asidToKey(asid IO_as) IO_key { + return Key_macK{asid} } ghost From 87d14cb5b24e3c78ef36d5efdea119db7d8d2564 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Jul 2024 09:13:12 +0200 Subject: [PATCH 4/7] might have to reverse this --- verification/io/router.gobra | 33 +++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 685d04810..385c55327 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -34,28 +34,36 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm { ghost decreases pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool { + return hf_valid_impl(dp.Asid(), ts, uinfo, hf) +} + +ghost +opaque +decreases +pure func hf_valid_impl(asid IO_as, 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 next := dp.nextMsgtermSpec(inif, egif, ts, uinfo) in + let next := nextMsgtermSpec(asid, inif, egif, ts, uinfo) in x == next } ghost -//opaque decreases -pure func (dp DataPlaneSpec) nextMsgtermSpec(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm { - // return let l := MsgTerm_L { - // seq[IO_msgterm]{ - // MsgTerm_Num{ts}, - // if2term(inif), - // if2term(egif), - // MsgTerm_FS{uinfo}}, - // } in mac(macKey(asidToKey(dp.Asid())), l) - return let l := plaintextToMac(inif, egif, ts, uinfo) in - mac(macKey(asidToKey(dp.Asid())), l) +pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm { + return let l := MsgTerm_L { + seq[IO_msgterm] { + MsgTerm_Num{ts}, + if2term(inif), + if2term(egif), + MsgTerm_FS{uinfo}, + }, + } in mac(macKey(asidToKey(asid)), l) + // return let l := plaintextToMac(inif, egif, ts, uinfo) in + // mac(macKey(asidToKey(dp.Asid())), l) } +/* ghost opaque decreases @@ -69,6 +77,7 @@ pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinf }, } } +*/ ghost decreases From 73948643427e689a6f9a475da0e247e6849b01e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Jul 2024 12:38:43 +0200 Subject: [PATCH 5/7] backup --- verification/io/other_defs.gobra | 1 + verification/io/router.gobra | 24 ++++++++---------------- 2 files changed, 9 insertions(+), 16 deletions(-) diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index a5c48ccae..7f600a457 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -200,6 +200,7 @@ type IO_dp2_state adt { } ghost +opaque decreases 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 385c55327..95c8faafb 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -43,29 +43,22 @@ decreases pure func hf_valid_impl(asid IO_as, 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 hvf := hf.HVF in let next := nextMsgtermSpec(asid, inif, egif, ts, uinfo) in - x == next + hvf == next } ghost +ensures result.extract_asid() == asid decreases -pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm { - return let l := MsgTerm_L { - seq[IO_msgterm] { - MsgTerm_Num{ts}, - if2term(inif), - if2term(egif), - MsgTerm_FS{uinfo}, - }, - } in mac(macKey(asidToKey(asid)), l) - // return let l := plaintextToMac(inif, egif, ts, uinfo) in - // mac(macKey(asidToKey(dp.Asid())), l) +pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) (result IO_msgterm) { + return let l := plaintextToMac(inif, egif, ts, uinfo) in + let res := mac(macKey(asidToKey(asid)), l) in + let _ := reveal res.extract_asid() in + res } -/* ghost -opaque decreases pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm { return MsgTerm_L { @@ -77,7 +70,6 @@ pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinf }, } } -*/ ghost decreases From 1eda55a25f3fcb582c2dddfca3fed30631ac9834 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Jul 2024 13:49:39 +0200 Subject: [PATCH 6/7] backup --- verification/io/router.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 95c8faafb..533bdee8d 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -38,7 +38,6 @@ pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf } ghost -opaque decreases pure func hf_valid_impl(asid IO_as, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool { return let inif := hf.InIF2 in @@ -49,6 +48,7 @@ pure func hf_valid_impl(asid IO_as, ts uint, uinfo set[IO_msgterm], hf IO_HF) bo } ghost +opaque ensures result.extract_asid() == asid decreases pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) (result IO_msgterm) { From 9afb3d8ecdaaad08af6124411df11f3307023b9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 25 Jul 2024 14:30:48 +0200 Subject: [PATCH 7/7] Update router/io-spec-abstract-transitions.gobra --- router/io-spec-abstract-transitions.gobra | 1 - 1 file changed, 1 deletion(-) diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index 083e01089..8aa346ff3 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -205,7 +205,6 @@ func ExternalEnterOrExitEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], ne reveal AbsValidateEgressIDConstraint(nextPkt, (ingressID != none[io.IO_ifs]), dp) reveal AbsProcessEgress(nextPkt) if(ingressID == none[io.IO_ifs]){ - // assert false AtomicExit(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) } else { AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)