diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml index 2579bb10b..f228507c6 100644 --- a/.github/workflows/gobra.yml +++ b/.github/workflows/gobra.yml @@ -21,40 +21,31 @@ env: checkConsistency: '1' imageVersion: 'latest' mceMode: 'od' - requireTriggers: '1' + # disabled for now, as it is unclear which triggers to + # provide to monoset in a way that it does not severely + # affect perf. + requireTriggers: '0' useZ3API: '0' viperBackend: 'SILICON' disableNL: '0' unsafeWildcardOptimization: '0' overflow: '0' respectFunctionPrePermAmounts: '0' + enableFriendClauses: '1' jobs: - verify-deps: + verify-third-party-libs: runs-on: ubuntu-latest steps: - name: Checkout the VerifiedSCION repository uses: actions/checkout@v3 - # Skip caching for now, the Github action right now is very limited. - # - name: Cache the verification results - # uses: actions/cache@v3 - # env: - # cache-name: gobra-cache - # with: - # path: ${{ runner.workspace }}/.gobra/cache.json - # key: ${{ env.cache-name }} - - # We split the verification of the entire repository into - # multiple steps. This provides a more fine-grained log in - # Github Workflow's interface and it allows more fine-grained - # control over the settings applied to each package (this last - # point could be also be solved by adapting the action to allow - # per package config). - name: Verify the packages in the 'verification' directory uses: viperproject/gobra-action@main with: projectLocation: 'VerifiedSCION/verification' recursive: 1 + ## Due to a bug, we cannot use the recursive mode with friend pacakge invariants. + excludePackages: 'layers' timeout: 5m headerOnly: ${{ env.headerOnly }} module: ${{ env.module }} @@ -71,6 +62,49 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} + # due to the bug mention above, we need to verify this package separately + - name: Verify package 'verification/dependencies/github.com/google/gopacket/layers' + uses: viperproject/gobra-action@main + with: + packages: 'verification/dependencies/github.com/google/gopacket/layers' + timeout: 5m + headerOnly: ${{ env.headerOnly }} + module: ${{ env.module }} + includePaths: 'verification/dependencies/ .' # relative to project location + assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }} + checkConsistency: ${{ env.checkConsistency }} + parallelizeBranches: ${{ env.parallelizeBranches }} + imageVersion: ${{ env.imageVersion }} + mceMode: ${{ env.mceMode }} + requireTriggers: ${{ env.requireTriggers }} + overflow: ${{ env.overflow }} + useZ3API: ${{ env.useZ3API }} + disableNL: ${{ env.disableNL }} + viperBackend: ${{ env.viperBackend }} + unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} + respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} + verify-deps: + runs-on: ubuntu-latest + steps: + - name: Checkout the VerifiedSCION repository + uses: actions/checkout@v3 + # Skip caching for now, the Github action right now is very limited. + # - name: Cache the verification results + # uses: actions/cache@v3 + # env: + # cache-name: gobra-cache + # with: + # path: ${{ runner.workspace }}/.gobra/cache.json + # key: ${{ env.cache-name }} + + # We split the verification of the entire repository into + # multiple steps. This provides a more fine-grained log in + # Github Workflow's interface and it allows more fine-grained + # control over the settings applied to each package (this last + # point could be also be solved by adapting the action to allow + # per package config). - name: Verify package 'pkg/addr' uses: viperproject/gobra-action@main with: @@ -92,6 +126,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/experimental/epic' uses: viperproject/gobra-action@main with: @@ -112,6 +147,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/log' uses: viperproject/gobra-action@main with: @@ -132,6 +168,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/private/serrors' uses: viperproject/gobra-action@main with: @@ -152,6 +189,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/scrypto' uses: viperproject/gobra-action@main with: @@ -172,6 +210,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/slayers' uses: viperproject/gobra-action@main with: @@ -192,6 +231,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/slayers/path' uses: viperproject/gobra-action@main with: @@ -212,6 +252,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/slayers/path/empty' uses: viperproject/gobra-action@main with: @@ -232,6 +273,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/slayers/path/epic' uses: viperproject/gobra-action@main with: @@ -253,6 +295,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/slayers/path/onehop' uses: viperproject/gobra-action@main with: @@ -273,6 +316,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'pkg/slayers/path/scion' uses: viperproject/gobra-action@main with: @@ -293,6 +337,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'private/topology' uses: viperproject/gobra-action@main with: @@ -313,6 +358,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'private/topology/underlay' uses: viperproject/gobra-action@main with: @@ -333,6 +379,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'private/underlay/conn' uses: viperproject/gobra-action@main with: @@ -353,6 +400,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'private/underlay/sockctrl' uses: viperproject/gobra-action@main with: @@ -373,6 +421,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'router/bfd' uses: viperproject/gobra-action@main with: @@ -393,6 +442,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Verify package 'router/control' uses: viperproject/gobra-action@main with: @@ -413,6 +463,7 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }} respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} - name: Upload the verification report uses: actions/upload-artifact@v4 with: @@ -446,3 +497,4 @@ jobs: viperBackend: ${{ env.viperBackend }} unsafeWildcardOptimization: '0' respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }} + enableFriendClauses: ${{ env.enableFriendClauses }} diff --git a/pkg/addr/host.go b/pkg/addr/host.go index 8efeb76aa..ce971e76c 100644 --- a/pkg/addr/host.go +++ b/pkg/addr/host.go @@ -15,9 +15,16 @@ // +gobra -// @ initEnsures ErrBadHostAddrType.ErrorMem() -// @ initEnsures ErrMalformedHostAddrType.ErrorMem() -// @ initEnsures ErrUnsupportedSVCAddress.ErrorMem() +// @ dup pkgInvariant ErrBadHostAddrType != nil && +// @ ErrMalformedHostAddrType != nil && +// @ ErrUnsupportedSVCAddress != nil && +// @ acc(ErrBadHostAddrType.ErrorMem(), _) && +// @ acc(ErrMalformedHostAddrType.ErrorMem(), _) && +// @ acc(ErrUnsupportedSVCAddress.ErrorMem(), _) && +// @ ErrBadHostAddrType.IsDuplicableMem() && +// @ ErrMalformedHostAddrType.IsDuplicableMem() && +// @ ErrUnsupportedSVCAddress.IsDuplicableMem() + package addr import ( @@ -206,7 +213,7 @@ func (h HostIPv4) IP() (res net.IP) { func (h HostIPv4) Copy() (res HostAddr) { //@ unfold acc(h.Mem(), R13) //@ unfold acc(sl.Bytes(h, 0, len(h)), R13) - var tmp HostIPv4 = HostIPv4(append( /*@ R13, @*/ net.IP(nil), h...)) + tmp := HostIPv4(append( /*@ R13, @*/ net.IP(nil), h...)) //@ fold acc(sl.Bytes(h, 0, len(h)), R13) //@ fold sl.Bytes(tmp, 0, len(tmp)) //@ fold acc(h.Mem(), R13) @@ -274,7 +281,7 @@ func (h HostIPv6) IP() (res net.IP) { func (h HostIPv6) Copy() (res HostAddr) { //@ unfold acc(h.Mem(), R13) //@ unfold acc(sl.Bytes(h, 0, len(h)), R13) - var tmp HostIPv6 = HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...)) + tmp := HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...)) //@ fold acc(sl.Bytes(h, 0, len(h)), R13) //@ fold sl.Bytes(tmp, 0, len(tmp)) //@ fold acc(h.Mem(), R13) diff --git a/pkg/addr/host_spec.gobra b/pkg/addr/host_spec.gobra index ed6e9032f..4108094ab 100644 --- a/pkg/addr/host_spec.gobra +++ b/pkg/addr/host_spec.gobra @@ -19,6 +19,7 @@ package addr import ( "net" + "github.com/scionproto/scion/verification/utils/errors" "github.com/scionproto/scion/verification/utils/slices" ) @@ -70,3 +71,27 @@ pure func sizeOfHostAddrType(htype HostAddrType) (res int) { HostLenIPv4 : htype == HostTypeIPv6 ? HostLenIPv6 : HostLenSVC } + +ghost +ensures ErrBadHostAddrType.ErrorMem() +decreases +func EstablishErrBadHostAddrTypeMem() { + openDupPkgInv + errors.DupErrorsCanBePromoted(ErrBadHostAddrType) +} + +ghost +ensures ErrMalformedHostAddrType.ErrorMem() +decreases +func EstablishErrMalformedHostAddrTypeMem() { + openDupPkgInv + errors.DupErrorsCanBePromoted(ErrMalformedHostAddrType) +} + +ghost +ensures ErrUnsupportedSVCAddress.ErrorMem() +decreases +func EstablishErrUnsupportedSVCAddressMem() { + openDupPkgInv + errors.DupErrorsCanBePromoted(ErrUnsupportedSVCAddress) +} \ No newline at end of file diff --git a/pkg/experimental/epic/epic.go b/pkg/experimental/epic/epic.go index a316fd5a0..77a131064 100644 --- a/pkg/experimental/epic/epic.go +++ b/pkg/experimental/epic/epic.go @@ -14,7 +14,7 @@ // +gobra -// @ initEnsures acc(postInitInvariant(), _) +// @ dup pkgInvariant acc(postInitInvariant(), _) package epic import ( diff --git a/pkg/experimental/epic/epic_spec.gobra b/pkg/experimental/epic/epic_spec.gobra index 8b0e7a795..68bf2565c 100644 --- a/pkg/experimental/epic/epic_spec.gobra +++ b/pkg/experimental/epic/epic_spec.gobra @@ -26,7 +26,8 @@ pred postInitInvariant() { // learn the invariant established by init ghost -trusted // TODO: drop after init invs are added ensures acc(postInitInvariant(), _) -decreases _ -func establishPostInitInvariant() \ No newline at end of file +decreases +func establishPostInitInvariant() { + openDupPkgInv +} \ No newline at end of file diff --git a/pkg/private/serrors/serrors_spec.gobra b/pkg/private/serrors/serrors_spec.gobra index 3bd25fe75..c08711af8 100644 --- a/pkg/private/serrors/serrors_spec.gobra +++ b/pkg/private/serrors/serrors_spec.gobra @@ -93,5 +93,8 @@ func WrapStr(msg string, cause error, errCtx ...interface{}) (res error) preserves forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> acc(&errCtx[i], R15) ensures res != nil && res.ErrorMem() ensures res.IsDuplicableMem() +// New always returns a pointer to a basicError, thus it +// only produces comparable values +ensures isComparable(res) decreases func New(msg string, errCtx ...interface{}) (res error) diff --git a/pkg/slayers/layertypes_spec.gobra b/pkg/slayers/layertypes_spec.gobra index 6e5d1dd5e..84d36b55a 100644 --- a/pkg/slayers/layertypes_spec.gobra +++ b/pkg/slayers/layertypes_spec.gobra @@ -18,16 +18,11 @@ // +gobra // To be added on a per-need basis -initEnsures LayerTypeSCION == 1000 +dup pkgInvariant LayerTypeSCION == 1000 package slayers import ( "github.com/google/gopacket" - - // the following comes from gopacket/layers instead of gopacket - importRequires gopacket.LayerTypesMem() - importRequires forall t gopacket.LayerType :: { gopacket.Registered(t) } 1000 <= t ==> - !gopacket.Registered(t) "github.com/google/gopacket/layers" ) @@ -60,6 +55,7 @@ var ( // post init properties ghost +trusted ensures res === LayerClassSCION ensures res != nil ensures res == (gopacket.LayerClass)(gopacket.LayerType(1000)) @@ -67,6 +63,7 @@ decreases func LayerClassSCIONIsLayerType() (res gopacket.LayerClass) ghost +trusted ensures res === LayerClassSCMP ensures res != nil ensures res == (gopacket.LayerClass)(gopacket.LayerType(1002)) @@ -74,6 +71,7 @@ decreases func LayerClassSCMPIsLayerType() (res gopacket.LayerClass) ghost +trusted ensures res === LayerClassHopByHopExtn ensures res != nil ensures res == (gopacket.LayerClass)(gopacket.LayerType(1003)) diff --git a/pkg/slayers/path/empty/empty.go b/pkg/slayers/path/empty/empty.go index 73e92dc15..30b7c12ed 100644 --- a/pkg/slayers/path/empty/empty.go +++ b/pkg/slayers/path/empty/empty.go @@ -26,12 +26,10 @@ const PathLen = 0 const PathType path.Type = 0 -// @ requires path.PathPackageMem() -// @ requires !path.Registered(PathType) -// @ ensures path.PathPackageMem() -// @ ensures forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==> -// @ t != PathType ==> old(path.Registered(t)) == path.Registered(t) -// @ ensures path.Registered(PathType) +// @ requires path.PkgMem() +// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType)) +// @ ensures path.PkgMem() +// @ ensures path.RegisteredTypes().Contains(int64(PathType)) // @ decreases func RegisterPath() { tmp := path.Metadata{ @@ -48,7 +46,7 @@ func RegisterPath() { }, } //@ proof tmp.New implements path.NewPathSpec { - //@ return tmp.New() as newPath + //@ return tmp.New() as newPath //@ } path.RegisterPath(tmp) } diff --git a/pkg/slayers/path/epic/epic.go b/pkg/slayers/path/epic/epic.go index c9d770163..4884f5162 100644 --- a/pkg/slayers/path/epic/epic.go +++ b/pkg/slayers/path/epic/epic.go @@ -41,12 +41,10 @@ const ( ) // RegisterPath registers the EPIC path type globally. -// @ requires path.PathPackageMem() -// @ requires !path.Registered(PathType) -// @ ensures path.PathPackageMem() -// @ ensures forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==> -// @ t != PathType ==> old(path.Registered(t)) == path.Registered(t) -// @ ensures path.Registered(PathType) +// @ requires path.PkgMem() +// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType)) +// @ ensures path.PkgMem() +// @ ensures path.RegisteredTypes().Contains(int64(PathType)) // @ decreases func RegisterPath() { tmp := path.Metadata{ @@ -65,7 +63,7 @@ func RegisterPath() { }, } //@ proof tmp.New implements path.NewPathSpec { - //@ return tmp.New() as newPath + //@ return tmp.New() as newPath //@ } path.RegisterPath(tmp) } diff --git a/pkg/slayers/path/onehop/onehop.go b/pkg/slayers/path/onehop/onehop.go index 868147f76..31e832b34 100644 --- a/pkg/slayers/path/onehop/onehop.go +++ b/pkg/slayers/path/onehop/onehop.go @@ -29,12 +29,10 @@ const PathLen = path.InfoLen + 2*path.HopLen const PathType path.Type = 2 -// @ requires path.PathPackageMem() -// @ requires !path.Registered(PathType) -// @ ensures path.PathPackageMem() -// @ ensures forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==> -// @ t != PathType ==> old(path.Registered(t)) == path.Registered(t) -// @ ensures path.Registered(PathType) +// @ requires path.PkgMem() +// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType)) +// @ ensures path.PkgMem() +// @ ensures path.RegisteredTypes().Contains(int64(PathType)) // @ decreases func RegisterPath() { tmp := path.Metadata{ @@ -51,7 +49,7 @@ func RegisterPath() { }, } //@ proof tmp.New implements path.NewPathSpec { - //@ return tmp.New() as newPath + //@ return tmp.New() as newPath //@ } path.RegisterPath(tmp) } diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go index 9643e4aef..2d0bdc5af 100644 --- a/pkg/slayers/path/path.go +++ b/pkg/slayers/path/path.go @@ -14,18 +14,21 @@ // +gobra -// @ initEnsures PathPackageMem() -// Skipped the following post-condition due to performance reasons -// initEnsures forall t Type :: 0 <= t && t < maxPathType ==> !Registered(t) -// Instead, we have: -// @ initEnsures !Registered(0) && !Registered(1) && !Registered(2) && !Registered(3) package path +// @ friendPkg "../" PkgMem() +// We have a non-quantified friendPkg clause below to avoid perf. issues. +// @ friendPkg "../" RegisteredTypes().DoesNotContain(0) && +// @ RegisteredTypes().DoesNotContain(1) && +// @ RegisteredTypes().DoesNotContain(2) && +// @ RegisteredTypes().DoesNotContain(3) + import ( "fmt" "github.com/scionproto/scion/pkg/private/serrors" //@ . "github.com/scionproto/scion/verification/utils/definitions" + //@ "github.com/scionproto/scion/verification/utils/monoset" //@ sl "github.com/scionproto/scion/verification/utils/slices" ) @@ -37,22 +40,24 @@ var ( strictDecoding/*@@@*/ bool = true ) +// @ ghost var registeredKeys monoset.BoundedMonotonicSet = monoset.Alloc(0, int64(maxPathType)) + func init() { // (VerifiedSCION) ghost initialization code to establish the PathPackageMem predicate. // @ assert acc(®isteredPaths) // @ assert acc(&strictDecoding) - // @ fold PathPackageMem() + // @ fold PkgMem() } // Type indicates the type of the path contained in the SCION header. type Type uint8 // @ requires 0 <= t && t < maxPathType -// @ preserves acc(PathPackageMem(), R20) +// @ preserves acc(PkgMem(), R20) // @ decreases func (t Type) String() string { - //@ unfold acc(PathPackageMem(), R20) - //@ ghost defer fold acc(PathPackageMem(), R20) + //@ unfold acc(PkgMem(), R20) + //@ ghost defer fold acc(PkgMem(), R20) pm := registeredPaths[t] if !pm.inUse { return fmt.Sprintf("UNKNOWN (%d)", t) @@ -144,23 +149,24 @@ type Metadata struct { // RegisterPath registers a new SCION path type globally. // The PathType passed in must be unique, or a runtime panic will occur. // @ requires 0 <= pathMeta.Type && pathMeta.Type < maxPathType -// @ requires PathPackageMem() -// @ requires !Registered(pathMeta.Type) +// @ requires PkgMem() +// @ requires RegisteredTypes().DoesNotContain(int64(pathMeta.Type)) // @ requires pathMeta.New implements NewPathSpec -// @ ensures PathPackageMem() -// @ ensures forall t Type :: { old(Registered(t)) }{ Registered(t) } 0 <= t && t < maxPathType ==> -// @ t != pathMeta.Type ==> old(Registered(t)) == Registered(t) -// @ ensures Registered(pathMeta.Type) +// @ ensures PkgMem() +// @ ensures RegisteredTypes().Contains(int64(pathMeta.Type)) // @ decreases func RegisterPath(pathMeta Metadata) { - //@ unfold PathPackageMem() + //@ unfold PkgMem() pm := registeredPaths[pathMeta.Type] + // @ RegisteredTypes().DoesNotContainImpliesNotFContains(int64(pathMeta.Type)) if pm.inUse { panic("path type already registered") } + // @ RegisteredTypes().Add(int64(pathMeta.Type)) registeredPaths[pathMeta.Type].inUse = true registeredPaths[pathMeta.Type].Metadata = pathMeta - //@ fold PathPackageMem() + // @ RegisteredTypes().ContainsImpliesFContains(int64(pathMeta.Type)) + //@ fold PkgMem() } // StrictDecoding enables or disables strict path decoding. If enabled, unknown @@ -170,23 +176,23 @@ func RegisterPath(pathMeta Metadata) { // Strict parsing is enabled by default. // // Experimental: This function is experimental and might be subject to change. -// @ requires PathPackageMem() -// @ ensures PathPackageMem() +// @ requires PkgMem() +// @ ensures PkgMem() // @ decreases func StrictDecoding(strict bool) { - //@ unfold PathPackageMem() + //@ unfold PkgMem() strictDecoding = strict - //@ fold PathPackageMem() + //@ fold PkgMem() } // NewPath returns a new path object of pathType. // @ requires 0 <= pathType && pathType < maxPathType -// @ requires acc(PathPackageMem(), _) +// @ requires acc(PkgMem(), _) // @ ensures e != nil ==> e.ErrorMem() // @ ensures e == nil ==> p != nil && p.NonInitMem() // @ decreases func NewPath(pathType Type) (p Path, e error) { - //@ unfold acc(PathPackageMem(), _) + //@ unfold acc(PkgMem(), _) pm := registeredPaths[pathType] if !pm.inUse { if strictDecoding { diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra index 57711e1d0..b22031a19 100644 --- a/pkg/slayers/path/path_spec.gobra +++ b/pkg/slayers/path/path_spec.gobra @@ -16,7 +16,10 @@ package path -import "github.com/scionproto/scion/verification/utils/slices" +import ( + "github.com/scionproto/scion/verification/utils/monoset" + "github.com/scionproto/scion/verification/utils/slices" +) /** rawPath spec **/ pred (r *rawPath) Mem(underlyingBuf []byte) { @@ -59,38 +62,50 @@ pure func (p *rawPath) LenSpec(ghost ub []byte) (l int) { /** Global state of the package **/ ghost const MaxPathType = maxPathType -pred PathPackageMem() { - acc(®isteredPaths) && - acc(&strictDecoding) && - forall t Type :: { ®isteredPaths[t].inUse } (0 <= t && t < maxPathType && registeredPaths[t].inUse) ==> registeredPaths[t].Metadata.New implements NewPathSpec +ghost +decreases +pure func RegisteredTypes() monoset.BoundedMonotonicSet { + return registeredKeys +} + +pred PkgMem() { + acc(®isteredPaths) && + acc(&strictDecoding) && + registeredKeys.Inv() && + registeredKeys.Start == 0 && + registeredKeys.End == maxPathType && + (forall t Type :: { ®isteredPaths[t].inUse } 0 <= t && t < maxPathType ==> + registeredPaths[t].inUse == registeredKeys.FContains(int64(t))) && + (forall t Type :: { ®isteredPaths[t].inUse } (0 <= t && t < maxPathType && registeredPaths[t].inUse) ==> + registeredPaths[t].Metadata.New implements NewPathSpec) } ghost requires 0 <= t && t < maxPathType -requires PathPackageMem() +requires PkgMem() decreases pure func Registered(t Type) (res bool) { - return unfolding PathPackageMem() in + return unfolding PkgMem() in registeredPaths[t].inUse } ghost requires 0 <= t && t < maxPathType -requires PathPackageMem() +requires PkgMem() decreases pure func GetType(t Type) (res Metadata) { - return unfolding PathPackageMem() in + return unfolding PkgMem() in registeredPaths[t].Metadata } ghost -requires PathPackageMem() +requires PkgMem() decreases pure func IsStrictDecoding() (b bool) { - return unfolding PathPackageMem() in - strictDecoding + return unfolding PkgMem() in strictDecoding } +// The following is a closure spec, not an assumed impl. // without passing `writePerm` explicitely below, we run into // exceptions when verifying method RegisterPath in package 'empty' ensures acc(p.NonInitMem(), writePerm) diff --git a/pkg/slayers/path/scion/base.go b/pkg/slayers/path/scion/base.go index 1754bd17a..1e0b48d53 100644 --- a/pkg/slayers/path/scion/base.go +++ b/pkg/slayers/path/scion/base.go @@ -39,12 +39,10 @@ const ( PathType path.Type = 1 ) -// @ requires path.PathPackageMem() -// @ requires !path.Registered(PathType) -// @ ensures path.PathPackageMem() -// @ ensures forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==> -// @ t != PathType ==> old(path.Registered(t)) == path.Registered(t) -// @ ensures path.Registered(PathType) +// @ requires path.PkgMem() +// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType)) +// @ ensures path.PkgMem() +// @ ensures path.RegisteredTypes().Contains(int64(PathType)) // @ decreases func RegisterPath() { tmp := path.Metadata{ diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index b9203fe0e..835aa15ca 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -13,12 +13,7 @@ // limitations under the License. // +gobra - -// @ initEnsures acc(path.PathPackageMem(), _) -// @ initEnsures path.Registered(empty.PathType) -// @ initEnsures path.Registered(scion.PathType) -// @ initEnsures path.Registered(onehop.PathType) -// @ initEnsures path.Registered(epic.PathType) +// @ dup pkgInvariant acc(path.PkgMem(), _) package slayers import ( @@ -30,9 +25,9 @@ import ( "github.com/scionproto/scion/pkg/addr" "github.com/scionproto/scion/pkg/private/serrors" - // @ importRequires path.PathPackageMem() - // @ importRequires !path.Registered(0) && !path.Registered(1) - // @ importRequires !path.Registered(2) && !path.Registered(3) + // @ importRequires path.PkgMem() + // @ importRequires path.RegisteredTypes().DoesNotContain(0) && path.RegisteredTypes().DoesNotContain(1) + // @ importRequires path.RegisteredTypes().DoesNotContain(2) && path.RegisteredTypes().DoesNotContain(3) "github.com/scionproto/scion/pkg/slayers/path" "github.com/scionproto/scion/pkg/slayers/path/empty" "github.com/scionproto/scion/pkg/slayers/path/epic" diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 3f92aff1e..4c04594cb 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -750,10 +750,11 @@ pure func isHostSVC(a net.Addr) bool { // invariant established by initialization ghost -trusted // TODO: drop this line after the static init PR -ensures acc(path.PathPackageMem(), _) +ensures acc(path.PkgMem(), _) decreases -func EstablishPathPkgMem() +func EstablishPathPkgMem() { + openDupPkgInv +} ghost requires s.Mem(ub) diff --git a/pkg/slayers/scmp_typecode.go b/pkg/slayers/scmp_typecode.go index b7d45666a..fb8475d25 100644 --- a/pkg/slayers/scmp_typecode.go +++ b/pkg/slayers/scmp_typecode.go @@ -14,7 +14,7 @@ // +gobra -// @ initEnsures SCMPTypeCodeMem() +// @ pkgInvariant SCMPTypeCodeMem() package slayers import ( diff --git a/pkg/slayers/scmp_typecode_spec.gobra b/pkg/slayers/scmp_typecode_spec.gobra index 3714232f3..b6bdbee3f 100644 --- a/pkg/slayers/scmp_typecode_spec.gobra +++ b/pkg/slayers/scmp_typecode_spec.gobra @@ -23,6 +23,7 @@ pred SCMPTypeCodeMem() { forall i SCMPType :: { scmpTypeCodeInfo[i] } i in domain(scmpTypeCodeInfo) ==> scmpTypeCodeInfo[i].codes != nil ==> acc(scmpTypeCodeInfo[i].codes) } +mayInit requires acc(scmpTypeCodeInfo) requires forall i SCMPType :: { scmpTypeCodeInfo[i] } i in domain(scmpTypeCodeInfo) ==> scmpTypeCodeInfo[i].codes != nil ==> acc(scmpTypeCodeInfo[i].codes) ensures SCMPTypeCodeMem() diff --git a/router/bfd/session_spec.gobra b/router/bfd/session_spec.gobra index 3791adfac..20f086367 100644 --- a/router/bfd/session_spec.gobra +++ b/router/bfd/session_spec.gobra @@ -20,12 +20,14 @@ // +gobra -initEnsures AlreadyRunning != nil && AlreadyRunning.ErrorMem() +dup pkgInvariant AlreadyRunning != nil && + acc(AlreadyRunning.ErrorMem(), _) && + AlreadyRunning.IsDuplicableMem() && + isComparable(AlreadyRunning) package bfd -import ( - "github.com/scionproto/scion/pkg/private/serrors" -) +import "github.com/scionproto/scion/pkg/private/serrors" +import "github.com/scionproto/scion/verification/utils/errors" var AlreadyRunning = serrors.New("is running") @@ -33,4 +35,7 @@ ghost ensures AlreadyRunning != nil && AlreadyRunning.ErrorMem() ensures isComparable(AlreadyRunning) decreases -func EstablishAlreadyRunning() \ No newline at end of file +func EstablishAlreadyRunning() { + openDupPkgInv + errors.DupErrorsCanBePromoted(AlreadyRunning) +} \ No newline at end of file diff --git a/router/dataplane.go b/router/dataplane.go index 7a9511fc6..c1aeb4703 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -15,17 +15,48 @@ // +gobra // (VerifiedSCION) the following init-postconditions causes severe slowdowns -// @ initEnsures alreadySet != nil && alreadySet.ErrorMem() -// @ initEnsures cannotRoute != nil && cannotRoute.ErrorMem() -// @ initEnsures emptyValue != nil && emptyValue.ErrorMem() -// @ initEnsures malformedPath != nil && malformedPath.ErrorMem() -// @ initEnsures modifyExisting != nil && modifyExisting.ErrorMem() -// @ initEnsures noSVCBackend != nil && noSVCBackend.ErrorMem() -// @ initEnsures unsupportedPathType != nil && unsupportedPathType.ErrorMem() -// @ initEnsures unsupportedPathTypeNextHeader != nil && unsupportedPathTypeNextHeader.ErrorMem() -// @ initEnsures noBFDSessionFound != nil && noBFDSessionFound.ErrorMem() -// @ initEnsures noBFDSessionConfigured != nil && noBFDSessionConfigured.ErrorMem() -// @ initEnsures errBFDDisabled != nil && errBFDDisabled.ErrorMem() +// @ dup pkgInvariant alreadySet != nil && +// @ acc(alreadySet.ErrorMem(), _) && +// @ alreadySet.IsDuplicableMem() +// @ dup pkgInvariant invalidSrcIA != nil && +// @ acc(invalidSrcIA.ErrorMem(), _) && +// @ invalidSrcIA.IsDuplicableMem() +// @ dup pkgInvariant invalidDstIA != nil && +// @ acc(invalidDstIA.ErrorMem(), _) && +// @ invalidDstIA.IsDuplicableMem() +// @ dup pkgInvariant invalidSrcAddrForTransit != nil && +// @ acc(invalidSrcAddrForTransit.ErrorMem(), _) && +// @ invalidSrcAddrForTransit.IsDuplicableMem() +// @ dup pkgInvariant cannotRoute != nil && +// @ acc(cannotRoute.ErrorMem(), _) && +// @ cannotRoute.IsDuplicableMem() +// @ dup pkgInvariant emptyValue != nil && +// @ acc(emptyValue.ErrorMem(), _) && +// @ emptyValue.IsDuplicableMem() +// @ dup pkgInvariant malformedPath != nil && +// @ acc(malformedPath.ErrorMem(), _) && +// @ malformedPath.IsDuplicableMem() +// @ dup pkgInvariant modifyExisting != nil && +// @ acc(modifyExisting.ErrorMem(), _) && +// @ modifyExisting.IsDuplicableMem() +// @ dup pkgInvariant noSVCBackend != nil && +// @ acc(noSVCBackend.ErrorMem(), _) && +// @ noSVCBackend.IsDuplicableMem() +// @ dup pkgInvariant unsupportedPathType != nil && +// @ acc(unsupportedPathType.ErrorMem(), _) && +// @ unsupportedPathType.IsDuplicableMem() +// @ dup pkgInvariant unsupportedPathTypeNextHeader != nil && +// @ acc(unsupportedPathTypeNextHeader.ErrorMem(), _) && +// @ unsupportedPathTypeNextHeader.IsDuplicableMem() +// @ dup pkgInvariant noBFDSessionFound != nil && +// @ acc(noBFDSessionFound.ErrorMem(), _) && +// @ noBFDSessionFound.IsDuplicableMem() +// @ dup pkgInvariant noBFDSessionConfigured != nil && +// @ acc(noBFDSessionConfigured.ErrorMem(), _) && +// @ noBFDSessionConfigured.IsDuplicableMem() +// @ dup pkgInvariant errBFDDisabled != nil && +// @ acc(errBFDDisabled.ErrorMem(), _) && +// @ errBFDDisabled.IsDuplicableMem() package router import ( diff --git a/router/assumptions.gobra b/router/post-init-invs.gobra similarity index 65% rename from router/assumptions.gobra rename to router/post-init-invs.gobra index 7634e35d6..aa0eca9f0 100644 --- a/router/assumptions.gobra +++ b/router/post-init-invs.gobra @@ -22,68 +22,99 @@ package router -/**** Post-init invariants ****/ +import "github.com/scionproto/scion/verification/utils/errors" -// All global variables of type 'error' declared in dataplane.go -// are duplicable. As such, we can always establish their invariants -// AFTER INITIALIZATION. +/**** Post-init invariants ****/ ghost ensures unsupportedPathType.ErrorMem() -decreases _ -func establishMemUnsupportedPathType() +decreases +func establishMemUnsupportedPathType() { + openDupPkgInv + errors.DupErrorsCanBePromoted(unsupportedPathType) +} ghost ensures malformedPath != nil ensures malformedPath.ErrorMem() -decreases _ -func establishMemMalformedPath() +decreases +func establishMemMalformedPath() { + openDupPkgInv + errors.DupErrorsCanBePromoted(malformedPath) +} ghost ensures alreadySet != nil ensures alreadySet.ErrorMem() -decreases _ -func establishAlreadySet() +decreases +func establishAlreadySet() { + openDupPkgInv + errors.DupErrorsCanBePromoted(alreadySet) +} ghost ensures unsupportedPathTypeNextHeader.ErrorMem() -decreases _ -func establishMemUnsupportedPathTypeNextHeader() +decreases +func establishMemUnsupportedPathTypeNextHeader() { + openDupPkgInv + errors.DupErrorsCanBePromoted(unsupportedPathTypeNextHeader) +} ghost ensures noBFDSessionConfigured.ErrorMem() -decreases _ -func establishMemNoBFDSessionConfigured() +decreases +func establishMemNoBFDSessionConfigured() { + openDupPkgInv + errors.DupErrorsCanBePromoted(noBFDSessionConfigured) +} ghost ensures noBFDSessionFound.ErrorMem() -decreases _ -func establishMemNoBFDSessionFound() +decreases +func establishMemNoBFDSessionFound() { + openDupPkgInv + errors.DupErrorsCanBePromoted(noBFDSessionFound) +} ghost ensures invalidSrcAddrForTransit.ErrorMem() -decreases _ -func establishInvalidSrcAddrForTransit() +decreases +func establishInvalidSrcAddrForTransit() { + openDupPkgInv + errors.DupErrorsCanBePromoted(invalidSrcAddrForTransit) +} ghost ensures noSVCBackend.ErrorMem() -decreases _ -func establishNoSVCBackend() +decreases +func establishNoSVCBackend() { + openDupPkgInv + errors.DupErrorsCanBePromoted(noSVCBackend) +} ghost ensures cannotRoute.ErrorMem() -decreases _ -func establishCannotRoute() +decreases +func establishCannotRoute() { + openDupPkgInv + errors.DupErrorsCanBePromoted(cannotRoute) +} ghost ensures invalidSrcIA.ErrorMem() -decreases _ -func establishInvalidSrcIA() +decreases +func establishInvalidSrcIA() { + openDupPkgInv + errors.DupErrorsCanBePromoted(invalidSrcIA) +} ghost ensures invalidDstIA.ErrorMem() -decreases _ -func establishInvalidDstIA() +decreases +func establishInvalidDstIA() { + openDupPkgInv + errors.DupErrorsCanBePromoted(invalidDstIA) +} /**** End of post-init invariants ****/ diff --git a/verification/dependencies/github.com/google/gopacket/decode.gobra b/verification/dependencies/github.com/google/gopacket/decode.gobra index 37d5e0469..a91ab9994 100644 --- a/verification/dependencies/github.com/google/gopacket/decode.gobra +++ b/verification/dependencies/github.com/google/gopacket/decode.gobra @@ -89,7 +89,7 @@ type PacketBuilder interface { type Decoder interface { pred Mem() - requires acc(LayerTypesMem(), _) + requires acc(PkgMem(), _) requires sl.Bytes(b, 0, len(b)) preserves Mem() preserves p.Mem() diff --git a/verification/dependencies/github.com/google/gopacket/layers/layertypes.gobra b/verification/dependencies/github.com/google/gopacket/layers/layertypes.gobra index 5ab8c0fb1..19a57e455 100644 --- a/verification/dependencies/github.com/google/gopacket/layers/layertypes.gobra +++ b/verification/dependencies/github.com/google/gopacket/layers/layertypes.gobra @@ -6,37 +6,19 @@ // +gobra -initEnsures gopacket.LayerTypesMem() -initEnsures LayerTypeBFD == gopacket.LayerType(122) -initEnsures gopacket.Registered(LayerTypeBFD) -initEnsures forall t gopacket.LayerType :: { gopacket.Registered(t) } (0 <= t && t <= 3) ==> - gopacket.Registered(t) -// The full postcondition cannot be proven because of performance reasons. -// Postconditions must be added with care to maintain the code verifiable and to not introduce unsoundness. -// Similarly, global variables declarations should be uncommented with care. -// initEnsures forall t gopacket.LayerType :: (10 <= t && t <= 146) ==> gopacket.Registered(t) -initEnsures forall t gopacket.LayerType :: { gopacket.Registered(t) } t < 0 ==> - !gopacket.Registered(t) -initEnsures forall t gopacket.LayerType :: { gopacket.Registered(t) } 146 < t ==> - !gopacket.Registered(t) +dup pkgInvariant LayerTypeBFD == 122 +dup pkgInvariant acc(gopacket.RegisteredTypes.Contains(122), _) + package layers -import ( - importRequires gopacket.LayerTypesMem() - importRequires forall t gopacket.LayerType :: { gopacket.Registered(t) } 0 <= t && t <= 3 ==> - gopacket.Registered(t) - importRequires forall t gopacket.LayerType :: { gopacket.Registered(t) } t < 0 ==> - !gopacket.Registered(t) - importRequires forall t gopacket.LayerType :: { gopacket.Registered(t) } 3 < t ==> - !gopacket.Registered(t) - "github.com/google/gopacket" -) +importRequires gopacket.RegisteredTypes.DoesNotContain(int64(122)) +import "github.com/google/gopacket" + +var LayerTypeBFD = gopacket.RegisterLayerType(122, gopacket.LayerTypeMetadata{Name: "BFD", Decoder: /* gopacket.DecodeFunc(decodeBFD)} */ generateDecoders()}) // This method just generates stubs for decoders so that we can avoid having to specify all 136 decoders +mayInit ensures d.Mem() decreases func generateDecoders() (d gopacket.Decoder) -var ( - LayerTypeBFD = gopacket.RegisterLayerType(122, gopacket.LayerTypeMetadata{Name: "BFD", Decoder: /* gopacket.DecodeFunc(decodeBFD)} */ generateDecoders()}) -) diff --git a/verification/dependencies/github.com/google/gopacket/layertype.gobra b/verification/dependencies/github.com/google/gopacket/layertype.gobra index 9afc2f935..b4429464b 100644 --- a/verification/dependencies/github.com/google/gopacket/layertype.gobra +++ b/verification/dependencies/github.com/google/gopacket/layertype.gobra @@ -6,19 +6,24 @@ // +gobra -initEnsures LayerTypesMem() -initEnsures LayerTypeZero == 0 -initEnsures LayerTypeDecodeFailure == 1 -initEnsures LayerTypePayload == 2 -initEnsures LayerTypeFragment == 3 -initEnsures Registered(LayerTypeZero) -initEnsures Registered(LayerTypeDecodeFailure) -initEnsures Registered(LayerTypePayload) -initEnsures Registered(LayerTypeFragment) -initEnsures forall t LayerType :: { Registered(t) } t < 0 ==> !Registered(t) -initEnsures forall t LayerType :: { Registered(t) } 3 < t ==> !Registered(t) +pkgInvariant PkgMem() +dup pkgInvariant acc(RegisteredTypes.Contains(int64(LayerTypeZero)), _) && + acc(RegisteredTypes.Contains(int64(LayerTypeDecodeFailure)), _) && + acc(RegisteredTypes.Contains(int64(LayerTypePayload)), _) && + acc(RegisteredTypes.Contains(int64(LayerTypeFragment)), _) +dup pkgInvariant LayerTypeZero == 0 && + LayerTypeDecodeFailure == 1 && + LayerTypePayload == 2 && + LayerTypeFragment == 3 + package gopacket +friendPkg "./layers" forall t LayerType :: { RegisteredTypes.DoesNotContain(int64(t)) } 10 <= t && t <= 146 ==> + RegisteredTypes.DoesNotContain(int64(t)) +friendPkg "../../../pkg/slayers" forall t LayerType :: { RegisteredTypes.DoesNotContain(int64(t)) } 1000 <= t && t <= 1100 ==> + RegisteredTypes.DoesNotContain(int64(t)) + +import ms "github.com/scionproto/scion/verification/utils/monoset" import sl "github.com/scionproto/scion/verification/utils/slices" /** Types **/ @@ -38,21 +43,42 @@ type LayerTypeMetadata struct { /** Constants **/ const maxLayerType = 2000 -ghost const MaxLayerType = maxLayerType // can be used for spec purposes + +ghost const MaxLayerType = maxLayerType +// Arbitrary bounds for valid LayerTypes. +// It is unlikely that this imposes any restriciton in practice. +ghost const AbsMinLayerType int64 = -1000 +ghost const AbsMaxLayerType int64 = 5000 +ghost var RegisteredTypes = ms.Alloc(AbsMinLayerType, AbsMaxLayerType) /** End of Constants **/ /** Predicates and ghost helper members **/ -pred LayerTypesMem() { - acc(<Meta) && acc(<MetaMap) && acc(ltMetaMap) && acc(&DecodersByLayerName, _) && acc(DecodersByLayerName) +pred PkgMem() { + acc(<Meta) && + acc(<MetaMap) && + acc(ltMetaMap) && + acc(&DecodersByLayerName, _) && + acc(DecodersByLayerName) && + RegisteredTypes.Inv() && + AbsMinLayerType <= 0 && + int64(maxLayerType) <= AbsMaxLayerType && + RegisteredTypes.Start == AbsMinLayerType && + RegisteredTypes.End == AbsMaxLayerType && + (forall t LayerType :: { <Meta[t].inUse } 0 <= t && t < maxLayerType ==> + ltMeta[t].inUse == RegisteredTypes.FContains(int64(t))) && + (forall t LayerType :: { ltMetaMap[t].inUse } ((AbsMinLayerType <= t && t < 0) || (maxLayerType <= t && t <= AbsMaxLayerType)) ==> + ltMetaMap[t].inUse == RegisteredTypes.FContains(int64(t))) } ghost -requires LayerTypesMem() +requires PkgMem() decreases pure func Registered(t LayerType) (res bool) { - return unfolding acc(LayerTypesMem(), _) in - (0 <= t && t < MaxLayerType? ltMeta[t].inUse : (t in domain(ltMetaMap) && ltMetaMap[t].inUse)) + return unfolding acc(PkgMem(), _) in + 0 <= t && t < MaxLayerType? + ltMeta[t].inUse : + (t in domain(ltMetaMap) && ltMetaMap[t].inUse) } ghost @@ -67,25 +93,52 @@ pure func registeredDuringInit(t LayerType) (res bool) { } // cannot be made ghost, even though it is morally so +mayInit requires acc(<Meta) && acc(<MetaMap) && acc(ltMetaMap) && acc(&DecodersByLayerName, _) && acc(DecodersByLayerName) requires forall t LayerType :: { registeredDuringInit(t) } !registeredDuringInit(t) -ensures LayerTypesMem() +requires RegisteredTypes.Inv() +requires RegisteredTypes.Start == AbsMinLayerType +requires RegisteredTypes.End == AbsMaxLayerType +requires forall t LayerType :: { <Meta[t].inUse } 0 <= t && t < maxLayerType ==> + ltMeta[t].inUse == RegisteredTypes.FContains(int64(t)) +requires forall t LayerType :: { ltMetaMap[t].inUse } (AbsMinLayerType <= t && t < 0) || (maxLayerType <= t && t <= AbsMaxLayerType) ==> + ltMetaMap[t].inUse == RegisteredTypes.FContains(int64(t)) +ensures PkgMem() ensures forall t LayerType :: { Registered(t) } !Registered(t) decreases func satisfyGlobalVarInitPre() int { - fold LayerTypesMem() + fold PkgMem() assert forall t LayerType :: { Registered(t) } old(!registeredDuringInit(t)) ==> !Registered(t) - assert unfolding LayerTypesMem() in forall t LayerType :: { registeredDuringInit(t) } !registeredDuringInit(t) + assert unfolding PkgMem() in forall t LayerType :: { registeredDuringInit(t) } !registeredDuringInit(t) assert forall t LayerType :: { Registered(t) } !Registered(t) return 1 } /** End of predicates and ghost helper members **/ +trusted +mayInit +ensures d.Mem() && d.Mem() // d.Mem() must be duplicable! +decreases _ +func generateDecodeUnknown() (d Decoder) + +trusted +mayInit +ensures d.Mem() +decreases _ +func generateDecodePayload() (d Decoder) + +trusted +mayInit +ensures d.Mem() +decreases _ +func generateDecodeFragment() (d Decoder) + /** Globals **/ + var ltMeta@ [maxLayerType]layerTypeMetadata var ltMetaMap@ = map[LayerType]layerTypeMetadata{} // DecodersByLayerName maps layer names to decoders for those layers. @@ -96,37 +149,16 @@ var DecodersByLayerName@ = map[string]Decoder{} /** Globals not originally declared in this file **/ /** Vars defined in decode.go that are required to establish preconditions of RegisterLayer. **/ // TODO: specify and verify the creation of these decoders -ensures d.Mem() && d.Mem() // d.Mem() must be duplicable! -decreases _ -func generateDecodeUnknown() (d Decoder) var DecodeUnknown = generateDecodeUnknown() - -ensures d.Mem() -decreases _ -func generateDecodePayload() (d Decoder) var DecodePayload = generateDecodePayload() - -ensures d.Mem() -decreases _ -func generateDecodeFragment() (d Decoder) var DecodeFragment = generateDecodeFragment() -/** End of Vars defined in decode.go that are required to establish preconditions of RegisterLayer. **/ // This call allows us to satisfy the preconditions of RegisterLayerType. var _ = satisfyGlobalVarInitPre() -// LayerTypeZero is an invalid layer type, but can be used to determine whether -// layer type has actually been set correctly. -var LayerTypeZero = RegisterLayerType(0, LayerTypeMetadata{Name: "Unknown", Decoder: DecodeUnknown}) -// LayerTypeDecodeFailure is the layer type for the default error layer. +var LayerTypeZero = RegisterLayerType(0, LayerTypeMetadata{Name: "Unknown", Decoder: DecodeUnknown}) var LayerTypeDecodeFailure = RegisterLayerType(1, LayerTypeMetadata{Name: "DecodeFailure", Decoder: DecodeUnknown}) - -// LayerTypePayload is the layer type for a payload that we don't try to decode -// but treat as a success, IE: an application-level payload. var LayerTypePayload = RegisterLayerType(2, LayerTypeMetadata{Name: "Payload", Decoder: DecodePayload}) - -// LayerTypeFragment is the layer type for a fragment of a layer transported -// by an underlying layer that supports fragmentation. var LayerTypeFragment = RegisterLayerType(3, LayerTypeMetadata{Name: "Fragment", Decoder: DecodeFragment}) /** End of globals not originally declared in this file **/ @@ -134,24 +166,28 @@ var LayerTypeFragment = RegisterLayerType(3, LayerTypeMetadata{Name: "Fragment", /** Ghost init operations **/ func init() { - assert forall t LayerType :: { Registered(t) } (t != 0 && t != 1 && t != 2 && t != 3) ==> - !Registered(t) - assert forall t LayerType :: { Registered(t) } t < 0 ==> !Registered(t) - assert forall t LayerType :: { Registered(t) } 3 < t ==> !Registered(t) + assert PkgMem() + assert RegisteredTypes.Contains(0) + assert RegisteredTypes.Contains(1) + assert RegisteredTypes.Contains(2) + assert RegisteredTypes.Contains(3) } /** End of ghost init operations **/ /** Actual Methods **/ -requires LayerTypesMem() -requires !Registered(LayerType(num)) +mayInit +requires AbsMinLayerType <= num && num <= AbsMaxLayerType +requires PkgMem() +requires RegisteredTypes.DoesNotContain(int64(num)) requires meta.Decoder != nil ==> meta.Decoder.Mem() -ensures LayerTypesMem() -ensures forall t LayerType :: { Registered(t) } t != LayerType(num) ==> old(Registered(t)) == Registered(t) +ensures PkgMem() +ensures RegisteredTypes.Contains(int64(num)) ensures Registered(LayerType(num)) ensures res == LayerType(num) decreases func RegisterLayerType(num int, meta LayerTypeMetadata) (res LayerType) { - unfold LayerTypesMem() + unfold PkgMem() + RegisteredTypes.DoesNotContainImpliesNotFContains(int64(num)) if 0 <= num && num < maxLayerType { if ltMeta[num].inUse { panic("Layer type already exists") @@ -161,20 +197,24 @@ func RegisterLayerType(num int, meta LayerTypeMetadata) (res LayerType) { panic("Layer type already exists") } } - fold LayerTypesMem() + fold PkgMem() return OverrideLayerType(num, meta) } -requires LayerTypesMem() +mayInit +requires PkgMem() +requires RegisteredTypes.DoesNotContain(int64(num)) requires meta.Decoder != nil ==> meta.Decoder.Mem() -ensures LayerTypesMem() -ensures forall t LayerType :: { Registered(t) } t != LayerType(num) ==> old(Registered(t)) == Registered(t) +ensures PkgMem() +ensures RegisteredTypes.Contains(int64(num)) ensures Registered(LayerType(num)) ensures res == LayerType(num) decreases func OverrideLayerType(num int, meta LayerTypeMetadata) (res LayerType) { - unfold LayerTypesMem() - defer fold LayerTypesMem() + unfold PkgMem() + RegisteredTypes.Add(int64(num)) + RegisteredTypes.ContainsImpliesFContains(int64(num)) + defer fold PkgMem() if 0 <= num && num < maxLayerType { ltMeta[num] = layerTypeMetadata{ inUse: true, @@ -190,8 +230,9 @@ func OverrideLayerType(num int, meta LayerTypeMetadata) (res LayerType) { return LayerType(num) } +trusted preserves c.Mem() preserves sl.Bytes(data, 0, len(data)) -ensures err != nil ==> err.ErrorMem() +ensures err != nil ==> err.ErrorMem() decreases func (t LayerType) Decode(data []byte, c PacketBuilder) (err error) diff --git a/verification/utils/errors/errors.gobra b/verification/utils/errors/errors.gobra new file mode 100644 index 000000000..c912ccff3 --- /dev/null +++ b/verification/utils/errors/errors.gobra @@ -0,0 +1,42 @@ +// Copyright 2022 ETH Zurich +// +// 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. + +// This file provides a specification to the package `serrors`. +// The specification cannot currently be added to the file 'errors.go' +// where the original definition of 'New' is because that file tries to +// import a third-party package for which we do not yet provide +// specification ("go.uber.org/zap/zapcore"). + +// Note that the original implementation of this package is not proven to satisfy +// the spec, it is only trusted to do so. + +// +gobra + +package errors + +// The following is an assumption that should not be +// problematic. It is useful to be able to declare +// the ErrorMem() as a dup. invariant of a package +// (the idea being that acc(ErrorMem(), _) is dup +// and then we can promote it). We can drop it as +// soon as Gobra allows passing proofs of duplicability +// for dup invariants. +ghost +trusted +requires e != nil +requires acc(e.ErrorMem(), _) +requires e.IsDuplicableMem() +ensures e.ErrorMem() +decreases _ +func DupErrorsCanBePromoted(e error) \ No newline at end of file diff --git a/verification/utils/monoset/monoset.gobra b/verification/utils/monoset/monoset.gobra new file mode 100644 index 000000000..edbf32778 --- /dev/null +++ b/verification/utils/monoset/monoset.gobra @@ -0,0 +1,306 @@ +// Copyright 2024 ETH Zurich +// +// 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 + +// This pkg should be the only monoset package. we do not need the other one. + +package monoset + +// BoundedMonotonicSet represents sets of uint8 to which we may add new elements, but +// never remove old ones. +type BoundedMonotonicSet struct { + ghost valuesMap dict[int64](gpointer[bool]) + ghost Start int64 + ghost End int64 +} + +pred (b BoundedMonotonicSet) Inv() { + (b.Start <= b.End) && + forall i int64 :: b.Start <= i && i <= b.End ==> + (i in domain(b.valuesMap) && acc(b.valuesMap[i], 1/2)) +} + +ghost +requires acc(b.Inv(), _) +requires b.Start <= i && i <= b.End +decreases +pure func (b BoundedMonotonicSet) FContains(i int64) bool { + // extra indirection avoids a type-checking bug of Gobra. + return unfolding acc(b.Inv(), _) in + b.fcontainshelper(i) +} + +ghost +requires forall i int64 :: b.Start <= i && i <= b.End ==> + (i in domain(b.valuesMap) && acc(b.valuesMap[i], _)) +requires b.Start <= i && i <= b.End +decreases +pure func (b BoundedMonotonicSet) fcontainshelper(i int64) bool { + return *b.valuesMap[i] +} + + +pred (b BoundedMonotonicSet) Contains(i int64) { + b.Start <= i && i <= b.End && + i in domain(b.valuesMap) && + acc(b.valuesMap[i], _) && + *b.valuesMap[i] +} + +ghost +requires b.Contains(i) +ensures b.Contains(i) && b.Contains(i) +decreases +func (b BoundedMonotonicSet) ContainsIsDup(i int64) { + unfold b.Contains(i) + fold b.Contains(i) + fold b.Contains(i) +} + +ghost +requires acc(b.Contains(i), _) +ensures b.Contains(i) +decreases +func (b BoundedMonotonicSet) PromoteContains(i int64) { + unfold acc(b.Contains(i), _) + fold b.Contains(i) +} + +pred (b BoundedMonotonicSet) DoesNotContain(i int64) { + b.Start <= i && i <= b.End && + i in domain(b.valuesMap) && + acc(b.valuesMap[i], 1/2) && + !(*b.valuesMap[i]) +} + +ghost +preserves acc(b.Inv(), 1/4) +preserves acc(b.DoesNotContain(i), 1/4) +ensures b.Start <= i && i <= b.End +ensures !b.FContains(i) +decreases +func (b BoundedMonotonicSet) DoesNotContainImpliesNotFContains(i int64) { + assert unfolding acc(b.Inv(), _) in + unfolding acc(b.DoesNotContain(i), _) in + !b.fcontainshelper(i) +} + +ghost +preserves acc(b.Inv(), 1/4) +preserves b.Contains(i) +ensures b.Start <= i && i <= b.End +ensures b.FContains(i) +decreases +func (b BoundedMonotonicSet) ContainsImpliesFContains(i int64) { + assert unfolding acc(b.Inv(), _) in + unfolding acc(b.Contains(i), _) in + b.fcontainshelper(i) +} + +ghost +requires start <= end +ensures res.Inv() +ensures res.Start == start && res.End == end +ensures forall i int64 :: start <= i && i <= end ==> + res.DoesNotContain(i) +// The following is technically redundant, but very useful. +ensures forall i int64 :: start <= i && i <= end ==> + !res.FContains(i) +decreases +func Alloc(start, end int64) (res BoundedMonotonicSet) { + b := BoundedMonotonicSet{ + Start: start, + End: end, + } + var i int64 + invariant start <= i && i <= end + invariant b.Start == start && b.End == end + invariant forall j int64 :: start <= j && j < i ==> + j in domain(b.valuesMap) + // injectivity requirement + invariant forall j1, j2 int64 :: start <= j1 && j1 < j2 && j2 < i ==> + b.valuesMap[j1] != b.valuesMap[j2] + invariant forall j int64 :: start <= j && j < i ==> + acc(b.valuesMap[j]) + invariant forall j int64 :: start <= j && j < i ==> + !(*b.valuesMap[j]) + decreases end - i + for i = start; i < end; i += 1 { + b.valuesMap[i] = new(bool) + } + // this repetition of the body of the loop here saves us from having + // the potential overflowing operation b.End+1 in the loop above. + b.valuesMap[i] = new(bool) + + invariant start <= i && i <= end + invariant b.Start == start && b.End == end + invariant forall j int64 :: start <= j && j <= end ==> + j in domain(b.valuesMap) + // injectivity requirement + invariant forall j1, j2 int64 :: start <= j1 && j1 < j2 && j2 < i ==> + b.valuesMap[j1] != b.valuesMap[j2] + invariant forall j int64 :: i <= j && j <= end ==> + acc(b.valuesMap[j]) && !(*b.valuesMap[j]) + invariant forall j int64 :: start <= j && j < i ==> + acc(b.valuesMap[j], 1/2) + invariant forall j int64 :: start <= j && j < i ==> + b.DoesNotContain(j) + invariant forall j int64 :: start <= j && j < i ==> + !b.fcontainshelper(j) + decreases end - i + for i = start; i < end; i += 1 { + fold b.DoesNotContain(i) + } + // this repetition of the body of the loop here saves us from having + // the potential overflowing operation b.End+1 in the loop above. + fold b.DoesNotContain(i) + fold b.Inv() + return b +} + +ghost +opaque // make this closed when that is supported +requires acc(b.Inv(), _) +decreases +pure func (b BoundedMonotonicSet) ToSet() set[int64] { + return unfolding acc(b.Inv(), _) in + b.toSetAux(b.Start) +} + +ghost +requires acc(b.Inv(), _) +requires b.Start <= start && start <= b.End +decreases b.End - start +pure func (b BoundedMonotonicSet) toSetAux(start int64) set[int64] { + return unfolding acc(b.Inv(), _) in + let part1 := (*b.valuesMap[start] ? set[int64]{start} : set[int64]{}) in + let part2 := (start < b.End ? b.toSetAux(start+1) : set[int64]{}) in + part1 union part2 +} + +ghost +requires 0 < p +requires acc(b.Inv(), p) +requires b.Contains(v) +ensures acc(b.Inv(), p) +ensures v in b.ToSet() +decreases +func (b BoundedMonotonicSet) ContainsImpliesAbstractContains(v int64, p perm) { + found := false + i := b.Start + part1 := set[int64]{} + part2 := reveal b.ToSet() + + assert unfolding b.Contains(v) in b.Start <= v && v <= b.End + + invariant acc(b.Inv(), p/2) + invariant b.Contains(v) + invariant b.Start <= i && i <= b.End + invariant v < i ==> found + invariant found ==> v in b.ToSet() + invariant part1 union part2 == b.ToSet() + invariant i <= b.End ==> + part2 == unfolding acc(b.Inv(), _) in ((*b.valuesMap[i] ? set[int64]{i} : set[int64]{}) union (i < b.End ? b.toSetAux(i+1) : set[int64]{})) + decreases b.End - i + for i = b.Start; i < b.End; i += 1 { + newpart1 := part1 union unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[int64]{i} : set[int64]{}) + newpart2 := i < b.End ? b.toSetAux(i+1) : set[int64]{} + if i == v { + unfold b.Contains(v) + found = true + assert *b.valuesMap[i] + assert newpart1 union newpart2 == b.ToSet() + assert v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[int64]{i} : set[int64]{})) + assert v in newpart1 + fold b.Contains(v) + } + part1 = newpart1 + part2 = newpart2 + } + // this repetition of the body of the loop here saves us from having + // the potential overflowing operation b.End+1 in the loop above. + if i == v { + unfold b.Contains(v) + found = true + assert *b.valuesMap[i] + assert v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[int64]{i} : set[int64]{})) + fold b.Contains(v) + } +} + +ghost +requires 0 < p +preserves acc(b.Inv(), p) +preserves b.DoesNotContain(v) +ensures !(v in b.ToSet()) +decreases +func (b BoundedMonotonicSet) DoesNotContainsImpliesAbstractDoesNotContain(v int64, p perm) { + found := false + i := int64(0) + part1 := set[int64]{} + part2 := reveal b.ToSet() + + assert unfolding b.DoesNotContain(v) in b.Start <= v && v <= b.End + + invariant acc(b.Inv(), p/2) + invariant b.DoesNotContain(v) + invariant b.Start <= i && i <= b.End + invariant !found + invariant found == v in part1 + invariant part1 union part2 == b.ToSet() + invariant i <= b.End ==> + part2 == unfolding acc(b.Inv(), _) in ((*b.valuesMap[i] ? set[int64]{i} : set[int64]{}) union (i < b.End ? b.toSetAux(i+1) : set[int64]{})) + invariant i == b.End ==> + part2 == unfolding acc(b.Inv(), _) in (*b.valuesMap[b.End] ? set[int64]{b.End} : set[int64]{}) + decreases b.End - i + for i = b.Start; i < b.End; i += 1 { + newpart1 := part1 union unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[int64]{i} : set[int64]{}) + newpart2 := i < b.End ? b.toSetAux(i+1) : set[int64]{} + if i == v { + unfold b.DoesNotContain(v) + assert !(*b.valuesMap[i]) + assert newpart1 union newpart2 == b.ToSet() + assert !(v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[int64]{i} : set[int64]{}))) + assert !(v in newpart1) + fold b.DoesNotContain(v) + } + part1 = newpart1 + part2 = newpart2 + } + // this repetition of the body of the loop here saves us from having + // the potential overflowing operation b.End+1 in the loop above. + if i == v { + unfold b.DoesNotContain(v) + assert !(*b.valuesMap[i]) + assert !(v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[int64]{i} : set[int64]{}))) + fold b.DoesNotContain(v) + } +} + +ghost +requires b.DoesNotContain(v) +preserves b.Inv() +ensures b.Contains(v) +ensures forall i int64 :: b.Start <= i && i <= b.End && i != v ==> + b.FContains(i) == old(b.FContains(i)) +decreases +func (b BoundedMonotonicSet) Add(v int64) { + unfold b.Inv() + unfold b.DoesNotContain(v) + ghost var ptr gpointer[bool] = b.valuesMap[v] + *ptr = true + fold b.Inv() + fold b.Contains(v) +} \ No newline at end of file