From fa9ff25e8554d967ac1e62345f873c02685830fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sat, 6 Apr 2024 22:27:18 +0200 Subject: [PATCH] streamline msgterm assumptions --- pkg/slayers/path/hopfield_spec.gobra | 15 ++------- pkg/slayers/path/infofield.go | 9 +++-- pkg/slayers/path/infofield_spec.gobra | 10 ++---- pkg/slayers/path/io_msgterm_spec.gobra | 46 ++++++++++++++++++++++++++ router/dataplane.go | 6 ++-- verification/io/router.gobra | 2 +- 6 files changed, 60 insertions(+), 28 deletions(-) create mode 100644 pkg/slayers/path/io_msgterm_spec.gobra diff --git a/pkg/slayers/path/hopfield_spec.gobra b/pkg/slayers/path/hopfield_spec.gobra index 011a2bc9d..e93e22f39 100644 --- a/pkg/slayers/path/hopfield_spec.gobra +++ b/pkg/slayers/path/hopfield_spec.gobra @@ -42,6 +42,7 @@ decreases pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle + 2 + k]) in let _ := Asserting(forall k int :: {&raw[middle+4:middle+6][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+6][k] == &raw[middle + 4 + k]) in + let _ := Asserting(forall k int :: {&raw[middle+6:middle+6+MacLen][k]} 0 <= k && k < MacLen ==> &raw[middle+6:middle+6+MacLen][k] == &raw[middle + 6 + k]) in unfolding acc(slices.AbsSlice_Bytes(raw, start, end), _) in let inif2 := binary.BigEndian.Uint16(raw[middle+2:middle+4]) in let egif2 := binary.BigEndian.Uint16(raw[middle+4:middle+6]) in @@ -50,7 +51,7 @@ pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { io.IO_HF(io.IO_HF_{ InIF2 : op_inif2, EgIF2 : op_egif2, - HVF : AbsMac(raw[6:6+MacLen]), + HVF : AbsMac(FromSliceToMacArray(raw[middle+6:middle+6+MacLen])), }) } @@ -60,16 +61,6 @@ pure func (h HopField) ToIO_HF() (io.IO_HF) { return io.IO_HF(io.IO_HF_{ InIF2 : ifsToIO_ifs(h.ConsIngress), EgIF2 : ifsToIO_ifs(h.ConsEgress), - HVF : AbsMac2(h.Mac), + HVF : AbsMac(h.Mac), }) } - -ghost -decreases -pure func AbsMac(mac []byte) (io.IO_msgterm) - - -ghost -decreases -pure func AbsMac2(mac [MacLen]byte) (io.IO_msgterm) - diff --git a/pkg/slayers/path/infofield.go b/pkg/slayers/path/infofield.go index bf362adda..b30edb937 100644 --- a/pkg/slayers/path/infofield.go +++ b/pkg/slayers/path/infofield.go @@ -131,16 +131,15 @@ func (inf *InfoField) SerializeTo(b []byte) (err error) { // UpdateSegID updates the SegID field by XORing the SegID field with the 2 // first bytes of the MAC. It is the beta calculation according to // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation +// @ requires hf.HVF == AbsMac(hfMac) // @ preserves acc(&inf.SegID) -// requires hf.HVF == AbsMac(hfMac[:]) -// @ ensures absUinfo_(inf.SegID) == old(io.upd_uinfo(absUinfo_(inf.SegID), hf)) +// @ ensures AbsUInfoFromUint16(inf.SegID) == +// @ old(io.upd_uinfo(AbsUInfoFromUint16(inf.SegID), hf)) // @ decreases func (inf *InfoField) UpdateSegID(hfMac [MacLen]byte /* @, ghost hf io.IO_HF @ */) { //@ share hfMac inf.SegID = inf.SegID ^ binary.BigEndian.Uint16(hfMac[:2]) - // TODO: (Markus) How to argue that we need to assume this - // upd_uinfo equivalent to xor in the protocol - // @ assume absUinfo_(inf.SegID) == old(io.upd_uinfo(absUinfo_(inf.SegID), hf)) + // @ AssumeForIO(AbsUInfoFromUint16(inf.SegID) == old(io.upd_uinfo(AbsUInfoFromUint16(inf.SegID), hf))) } // @ decreases diff --git a/pkg/slayers/path/infofield_spec.gobra b/pkg/slayers/path/infofield_spec.gobra index 8fc89aa61..b0da954d4 100644 --- a/pkg/slayers/path/infofield_spec.gobra +++ b/pkg/slayers/path/infofield_spec.gobra @@ -74,13 +74,9 @@ pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm] unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in let _ := Asserting(forall k int :: {&raw[idx:idx+2][k]} 0 <= k && k < 2 ==> &raw[idx:idx+4][k] == &raw[idx + k]) in - absUinfo_(binary.BigEndian.Uint16(raw[idx:idx+2])) + AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2])) } -ghost -decreases -pure func absUinfo_(SegID uint16) set[io.IO_msgterm] - // This type simplifies the infoField, making it easier // to use than the IO_seg3 from the IO-spec. type IntermediateAbsInfoField adt { @@ -113,7 +109,7 @@ pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in IntermediateAbsInfoField(IntermediateAbsInfoField_{ AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])), - UInfo : absUinfo_(binary.BigEndian.Uint16(raw[middle+2:middle+4])), + UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])), ConsDir : raw[middle] & 0x1 == 0x1, Peer : raw[middle] & 0x2 == 0x2, }) @@ -124,7 +120,7 @@ decreases pure func (inf InfoField) ToIntermediateAbsInfoField() (IntermediateAbsInfoField) { return IntermediateAbsInfoField(IntermediateAbsInfoField_{ AInfo : io.IO_ainfo(inf.Timestamp), - UInfo : absUinfo_(inf.SegID), + UInfo : AbsUInfoFromUint16(inf.SegID), ConsDir : inf.ConsDir, Peer : inf.Peer, }) diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra new file mode 100644 index 000000000..41e39093d --- /dev/null +++ b/pkg/slayers/path/io_msgterm_spec.gobra @@ -0,0 +1,46 @@ +// Copyright 2020 Anapaya Systems +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package path + +import "verification/io" + +// At the moment, we assume that all cryptographic operations performed at the code level +// imply the desired properties at the IO spec level because we cannot currently prove in +// Gobra the correctness of these operations. Given that we do not prove any properties +// about this function, we currently do not provide a definition for it. + +ghost +decreases +pure func AbsUInfoFromUint16(SegID uint16) set[io.IO_msgterm] + +ghost +decreases +pure func AbsMac(mac [MacLen]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. This functions is abstract for now +// because Gobra does not allow for array literals in pure functions, even though +// they are no more side-effectful than creating an instance of a struct type. +// This will soon be fixed in Gobra. +ghost +requires MacLen <= len(mac) +requires forall i int :: { &mac[i] } 0 <= i && i < MacLen ==> acc(&mac[i], _) +ensures len(res) == MacLen +ensures forall i int :: { res[i] } 0 <= i && i < MacLen ==> mac[i] == res[i] +decreases +pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte) diff --git a/router/dataplane.go b/router/dataplane.go index 89957df4f..2d57b28a9 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2328,7 +2328,7 @@ func (p *scionPacketProcessor) updateNonConsDirIngressSegID( /*@ ghost ub []byte // @ reveal p.EqAbsHopField(absPkt(dp, ub)) if !p.infoField.ConsDir && p.ingressID != 0 { p.infoField.UpdateSegID(p.hopField.Mac /*@, p.hopField.ToIO_HF() @*/) - // @ assert path.absUinfo_(p.infoField.SegID) == old(io.upd_uinfo(path.absUinfo_(p.infoField.SegID), p.hopField.ToIO_HF())) + // @ assert path.AbsUInfoFromUint16(p.infoField.SegID) == old(io.upd_uinfo(path.AbsUInfoFromUint16(p.infoField.SegID), p.hopField.ToIO_HF())) // (VerifiedSCION) the following property is guaranteed by the type system, but Gobra cannot infer it yet // @ assume 0 <= p.path.GetCurrINF(ubPath) // @ sl.SplitRange_Bytes(ub, start, end, HalfPerm) @@ -2342,7 +2342,7 @@ func (p *scionPacketProcessor) updateNonConsDirIngressSegID( /*@ ghost ub []byte // @ p.SubSliceAbsPktToAbsPkt(ub, start, end, dp) // @ ghost sl.CombineRange_Bytes(ub, start, end, HalfPerm) // @ absPktFutureLemma(dp, ub) - // @ assert absPkt(dp, ub).CurrSeg.UInfo == old(io.upd_uinfo(path.absUinfo_(p.infoField.SegID), p.hopField.ToIO_HF())) + // @ assert absPkt(dp, ub).CurrSeg.UInfo == old(io.upd_uinfo(path.AbsUInfoFromUint16(p.infoField.SegID), p.hopField.ToIO_HF())) // @ assert reveal p.EqAbsInfoField(absPkt(dp, ub)) // @ assert reveal p.EqAbsHopField(absPkt(dp, ub)) } @@ -2528,7 +2528,7 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte, ghost dp io.D // need to update the SegID. if p.infoField.ConsDir { p.infoField.UpdateSegID(p.hopField.Mac /*@, p.hopField.ToIO_HF() @*/) - // @ assert path.absUinfo_(p.infoField.SegID) == old(io.upd_uinfo(path.absUinfo_(p.infoField.SegID), p.hopField.ToIO_HF())) + // @ assert path.AbsUInfoFromUint16(p.infoField.SegID) == old(io.upd_uinfo(path.AbsUInfoFromUint16(p.infoField.SegID), p.hopField.ToIO_HF())) // @ assume 0 <= p.path.GetCurrINF(ubPath) if err := p.path.SetInfoField(p.infoField, int( /*@ unfolding acc(p.path.Mem(ubPath), R45) in (unfolding acc(p.path.Base.Mem(), R50) in @*/ p.path.PathMeta.CurrINF /*@ ) @*/) /*@ , ubPath, dp @*/); err != nil { // TODO parameter problem invalid path diff --git a/verification/io/router.gobra b/verification/io/router.gobra index d34d2de3a..e43b2efdf 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -72,7 +72,7 @@ pure func asidToKey(asid IO_as) IO_key{ ghost decreases -pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{ +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) }