From 4fc6c1f0def50697918267370754e6f1bf68b700 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 6 Mar 2025 14:06:42 +0100 Subject: [PATCH 1/3] updates to latest version of Gobra --- .gitlab-ci.yml | 2 +- arbitrary/arbitrary.gobra | 12 + .../attacker-completeness.gobra | 81 ++++-- .../concurrent-datastructure.gobra | 124 ++++----- concurrentdatastructure/ghost-mutex.gobra | 36 +++ event/event.gobra | 2 +- label/secrecy-label.gobra | 2 +- .../channel-communication.go | 50 +++- labeledlibrary/crypto.go | 217 ++++++++++++++- labeledlibrary/io.go | 34 ++- labeledlibrary/library/crypto.go | 252 ++++++++++++++++-- labeledlibrary/library/utils.go | 13 +- labeledlibrary/security-properties.gobra | 5 + labeledlibrary/state.go | 35 ++- labeling/key-type.gobra | 3 +- labeling/label-preservation.gobra | 27 ++ labeling/labeling.gobra | 5 +- local-verify.sh | 4 +- principal/principal.go | 6 +- term/bytes.gobra | 4 +- term/term.gobra | 6 +- trace/entry-helpers.gobra | 1 + trace/entry.gobra | 2 +- traceinvariant/trace-invariant.gobra | 18 +- tracemanager/entry-lemmas.gobra | 2 +- tracemanager/event-lemmas.gobra | 12 +- tracemanager/manager.gobra | 84 +++--- tracemanager/message-lemmas.gobra | 4 +- tracemanager/nonce-lemmas.gobra | 4 +- tracemanager/public-term-lemmas.gobra | 4 +- tracemanager/published-term-lemma.gobra | 4 +- tracemanager/search.gobra | 30 +-- usage/usage.gobra | 2 +- usagecontext/usage-context.gobra | 16 +- 34 files changed, 856 insertions(+), 247 deletions(-) create mode 100644 concurrentdatastructure/ghost-mutex.gobra diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index be6c76d..17b7f12 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,6 +1,6 @@ image: # name: ghcr.io/viperproject/gobra:latest - name: ghcr.io/viperproject/gobra@sha256:0e7419455a3648d006e8a9957380e94c1a8e52d2d4b1ce2425af852dc275fb29 # Gobra commit f21fe70 + name: ghcr.io/viperproject/gobra@sha256:432559ae1ea823d612e28f7e5798f1923cf7f4e343040359575c33ae081a01d9 # Gobra commit ab5ab7f # override entrypoint such that we get a shell in the image # as the image would otherwise expect a path to a Gobra file entrypoint: [""] diff --git a/arbitrary/arbitrary.gobra b/arbitrary/arbitrary.gobra index 77ed0bf..6a2b109 100644 --- a/arbitrary/arbitrary.gobra +++ b/arbitrary/arbitrary.gobra @@ -11,38 +11,50 @@ import u "github.com/ModularVerification/ReusableVerificationLibrary/usage" // these Go functions correspond to Viper methods that do not have any postcondition and thus do not constrain // their return value. +ghost decreases func GetArbTerm() tm.Term +ghost decreases func GetArbTraceEntry() tr.TraceEntry +ghost decreases func GetArbLabel() label.SecrecyLabel +ghost decreases func GetArbPrincipal() p.Principal +ghost decreases func GetArbId() p.Id +ghost decreases func GetArbEvent() ev.Event +ghost decreases func GetArbUsage() u.Usage +ghost decreases func GetArbString() string +ghost decreases func GetArbUInt32() uint32 +ghost decreases func GetArbUInt64() uint64 +ghost decreases func GetArbInt() int +ghost decreases func GetArbBool() bool diff --git a/attackercompleteness/attacker-completeness.gobra b/attackercompleteness/attacker-completeness.gobra index 50f0f5f..a475fc1 100644 --- a/attackercompleteness/attacker-completeness.gobra +++ b/attackercompleteness/attacker-completeness.gobra @@ -28,11 +28,19 @@ import u "github.com/ModularVerification/ReusableVerificationLibrary/usage" */ ghost +decreases if false // does not terminate requires l.Mem() ensures l.Mem() func Attacker(l *ll.LabeledLibrary) { + // to make Gobra happy, we introduce the notion of a bound on the number of steps + // the attacker can perform. However, this bound is arbitrary and, thus, does not + // affect soundness. + numberOfSteps := arb.GetArbInt() + invariant l.Mem() - for { + invariant 0 <= i && (i <= numberOfSteps || numberOfSteps < 0) + decreases numberOfSteps - i + for i := 0; i < numberOfSteps; i++ { // the attacker chooses non-deterministically an operation it wants to perform nonDeterministicChoice := arb.GetArbInt() if nonDeterministicChoice == 1 { @@ -81,6 +89,7 @@ func Attacker(l *ll.LabeledLibrary) { // operation 1: create nonce ghost +decreases requires l.Mem() ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) @@ -88,7 +97,7 @@ ensures err == nil ==> att.attackerKnows(l.Snapshot(), nonce) func CreateNonce(l *ll.LabeledLibrary, usageString string) (nonce tm.Term, err error) { unfold l.Mem() var nonceB lib.ByteString - nonceB, err = l.s.CreateNonce(tri.GetLabeling(l.ctx), label.Public(), usageString, set[ev.EventType]{}) + nonceB, err = l.s.GhostCreateNonce(tri.GetLabeling(l.ctx), label.Public(), usageString, set[ev.EventType]{}) if err == nil { nonce = tm.random(lib.Abs(nonceB), label.Public(), u.Nonce(usageString)) l.manager.LogNonce(l.ctx, l.owner, nonce) @@ -101,6 +110,7 @@ func CreateNonce(l *ll.LabeledLibrary, usageString string) (nonce tm.Term, err e // operation 2: send message ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), msg) ensures l.Mem() @@ -112,7 +122,7 @@ func Send(l *ll.LabeledLibrary, idSender, idReceiver p.Principal, msg tm.Term) ( unfold l.Mem() l.manager.LogSend(l.ctx, l.owner, idSender, idReceiver, msg) snapshot := l.manager.Snapshot(l.ctx, l.owner) - err = l.com.Send(idSender, idReceiver, msgBytes, msg, snapshot) + err = l.com.AttackerSend(idSender, idReceiver, msgBytes, msg, snapshot) fold l.Mem() } @@ -125,6 +135,7 @@ func Send(l *ll.LabeledLibrary, idSender, idReceiver p.Principal, msg tm.Term) ( // operation 4: extend attacker knowledge ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), t1) requires att.attackerKnows(l.Snapshot(), t2) @@ -319,14 +330,15 @@ func ExtendKnowledge(l *ll.LabeledLibrary, t1, t2, t3, t4, t5, t6, t7, t8 tm.Ter * representation */ ghost +decreases requires l.Mem() ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) ensures err == nil ==> att.attackerKnows(l.Snapshot(), sk) func GeneratePkeKey(l *ll.LabeledLibrary, usageString string) (sk tm.Term, err error) { unfold l.Mem() - var skB lib.ByteString - _, skB, err = l.s.GeneratePkeKey(tri.GetLabeling(l.ctx), label.Public(), usageString, set[ev.EventType]{}) + var pkB, skB lib.ByteString + pkB, skB, err = l.s.AttackerGeneratePkeKey(tri.GetLabeling(l.ctx), label.Public(), usageString, set[ev.EventType]{}) if err == nil { sk = tm.random(lib.Abs(skB), label.Public(), u.PkeKey(usageString)) l.manager.LogNonce(l.ctx, l.owner, sk) @@ -338,6 +350,7 @@ func GeneratePkeKey(l *ll.LabeledLibrary, usageString string) (sk tm.Term, err e } ghost +decreases requires l.Mem() ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) @@ -345,7 +358,7 @@ ensures err == nil ==> att.attackerKnows(l.Snapshot(), sk) func GenerateDHKey(l *ll.LabeledLibrary, usageString string) (sk tm.Term, err error) { unfold l.Mem() var skB lib.ByteString - skB, err = l.s.GenerateDHKey(tri.GetLabeling(l.ctx), label.Public(), usageString, set[ev.EventType]{}) + skB, err = l.s.AttackerGenerateDHKey(tri.GetLabeling(l.ctx), label.Public(), usageString, set[ev.EventType]{}) if err == nil { sk = tm.random(lib.Abs(skB), label.Public(), u.DhKey(usageString)) l.manager.LogNonce(l.ctx, l.owner, sk) @@ -357,6 +370,7 @@ func GenerateDHKey(l *ll.LabeledLibrary, usageString string) (sk tm.Term, err er } ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), pk) requires att.attackerKnows(l.Snapshot(), plaintext) @@ -368,7 +382,8 @@ func Enc(l *ll.LabeledLibrary, pk, plaintext tm.Term) (ciphertext tm.Term, err e plaintextBytes := lib.NewByteStringWithContent(tm.gamma(plaintext)) l.AttackerOnlyKnowsPublishableValues(pk) l.AttackerOnlyKnowsPublishableValues(plaintext) - _, err = l.Enc(plaintextBytes, pkBytes, plaintext, pk) + var ciphertextBytes lib.ByteString + ciphertextBytes, err = l.AttackerEnc(plaintextBytes, pkBytes, plaintext, pk) if err == nil { ciphertext = tm.encrypt(plaintext, pk) l.Publish(ciphertext) @@ -376,6 +391,7 @@ func Enc(l *ll.LabeledLibrary, pk, plaintext tm.Term) (ciphertext tm.Term, err e } ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), ciphertext) requires att.attackerKnows(l.Snapshot(), sk) @@ -389,7 +405,8 @@ func Dec(l *ll.LabeledLibrary, ciphertext, sk tm.Term) (plaintext tm.Term, err e l.AttackerOnlyKnowsPublishableValues(sk) skOwner := arb.GetArbId() l.LabelCtx().CanDecryptWithPublicSk(l.Snapshot(), ciphertext, sk, skOwner) - _, err = l.Dec(ciphertextBytes, skBytes, ciphertext, sk, skOwner) + var plaintextBytes lib.ByteString + plaintextBytes, err = l.AttackerDec(ciphertextBytes, skBytes, ciphertext, sk, skOwner) if err != nil { return } @@ -400,7 +417,7 @@ func Dec(l *ll.LabeledLibrary, ciphertext, sk tm.Term) (plaintext tm.Term, err e // we model the attacker to operate on symbolic terms. // thus, we additionally call decrypt on the term-level and abort // if decryption fails - err = lib.NewError("decryption failed") + err = lib.AttackerNewError("decryption failed") return } plaintext = get(optPlaintext) @@ -409,6 +426,7 @@ func Dec(l *ll.LabeledLibrary, ciphertext, sk tm.Term) (plaintext tm.Term, err e } ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), key) requires att.attackerKnows(l.Snapshot(), nonce) @@ -427,10 +445,11 @@ func AeadEnc(l *ll.LabeledLibrary, key, nonce, plaintext, additionalData tm.Term l.AttackerOnlyKnowsPublishableValues(plaintext) l.AttackerOnlyKnowsPublishableValues(additionalData) if lib.Size(keyBytes) != 32 || lib.Size(nonceBytes) != 12 { - err = lib.NewError("key or nonce have invalid length") + err = lib.AttackerNewError("key or nonce have invalid length") return } - _, err = l.AeadEnc(keyBytes, nonceBytes, plaintextBytes, additionalDataBytes, key, nonce, plaintext, additionalData, label.Public()) + var ciphertextBytes lib.ByteString + ciphertextBytes, err = l.AttackerAeadEnc(keyBytes, nonceBytes, plaintextBytes, additionalDataBytes, key, nonce, plaintext, additionalData, label.Public()) if err == nil { ciphertext = tm.aead(key, nonce, plaintext, additionalData) l.Publish(ciphertext) @@ -438,6 +457,7 @@ func AeadEnc(l *ll.LabeledLibrary, key, nonce, plaintext, additionalData tm.Term } ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), key) requires att.attackerKnows(l.Snapshot(), nonce) @@ -456,11 +476,12 @@ func AeadDec(l *ll.LabeledLibrary, key, nonce, ciphertext, additionalData tm.Ter l.AttackerOnlyKnowsPublishableValues(ciphertext) l.AttackerOnlyKnowsPublishableValues(additionalData) if lib.Size(keyBytes) != 32 || lib.Size(nonceBytes) != 12 { - err = lib.NewError("key or nonce have invalid length") + err = lib.AttackerNewError("key or nonce have invalid length") return } l.LabelCtx().CanAeadDecryptWithPublishableKey(l.Snapshot(), key, nonce, ciphertext, additionalData, label.Public()) - _, err = l.AeadDec(keyBytes, nonceBytes, ciphertextBytes, additionalDataBytes, key, nonce, ciphertext, additionalData, label.Public()) + var plaintextBytes lib.ByteString + plaintextBytes, err = l.AttackerAeadDec(keyBytes, nonceBytes, ciphertextBytes, additionalDataBytes, key, nonce, ciphertext, additionalData, label.Public()) if err != nil { return } @@ -471,7 +492,7 @@ func AeadDec(l *ll.LabeledLibrary, key, nonce, ciphertext, additionalData tm.Ter // we model the attacker to operate on symbolic terms. // thus, we additionally call decrypt on the term-level and abort // if decryption fails - err = lib.NewError("decryption failed") + err = lib.AttackerNewError("decryption failed") return } plaintext = get(optPlaintext) @@ -480,6 +501,7 @@ func AeadDec(l *ll.LabeledLibrary, key, nonce, ciphertext, additionalData tm.Ter } ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), msg) requires att.attackerKnows(l.Snapshot(), sk) @@ -492,7 +514,8 @@ func Sign(l *ll.LabeledLibrary, msg, sk tm.Term) (signedMsg tm.Term, err error) l.AttackerOnlyKnowsPublishableValues(msg) l.AttackerOnlyKnowsPublishableValues(sk) skOwner := arb.GetArbId() - _, err = l.Sign(msgBytes, skBytes, msg, sk, skOwner) + var signatureBytes lib.ByteString + signatureBytes, err = l.AttackerSign(msgBytes, skBytes, msg, sk, skOwner) if err == nil { signedMsg = tm.sign(msg, sk) l.Publish(signedMsg) @@ -500,6 +523,7 @@ func Sign(l *ll.LabeledLibrary, msg, sk tm.Term) (signedMsg tm.Term, err error) } ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), signedMsg) requires att.attackerKnows(l.Snapshot(), pk) @@ -518,7 +542,8 @@ func Open(l *ll.LabeledLibrary, signedMsg, pk tm.Term) (msg tm.Term, err error) sk := arb.GetArbTerm() assume lib.Abs(pkBytes) == tm.gamma(tm.createPk(sk)) skOwner := arb.GetArbId() - _, err = l.Open(signedMsgBytes, pkBytes, signedMsg, sk, skOwner) + var msgBytes lib.ByteString + msgBytes, err = l.AttackerOpen(signedMsgBytes, pkBytes, signedMsg, sk, skOwner) if err != nil { return } @@ -529,7 +554,7 @@ func Open(l *ll.LabeledLibrary, signedMsg, pk tm.Term) (msg tm.Term, err error) // we model the attacker to operate on symbolic terms. // thus, we additionally call open on the term-level and abort // if signature verification fails - err = lib.NewError("signature verification failed") + err = lib.AttackerNewError("signature verification failed") return } msg = get(optMsg) @@ -539,6 +564,7 @@ func Open(l *ll.LabeledLibrary, signedMsg, pk tm.Term) (msg tm.Term, err error) // operation 5: deconstruct term in the attacker knowledge ghost +decreases requires l.Mem() requires att.attackerKnows(l.Snapshot(), t) ensures l.Mem() @@ -584,6 +610,7 @@ func ExtendKnowledgeByDeconstruction(l *ll.LabeledLibrary, t tm.Term) { } ghost +decreases requires l.Mem() requires forall i uint :: { terms[i] } 0 <= i && i < len(terms) ==> l.LabelCtx().IsPublishable(l.Snapshot(), terms[i]) ensures l.Mem() @@ -596,6 +623,7 @@ func MultiPublish(l *ll.LabeledLibrary, terms seq[tm.Term]) { invariant forall j uint :: { terms[j] } i <= j && j < len(terms) ==> l.LabelCtx().IsPublishable(snap, terms[j]) invariant snap.isSuffix(l.Snapshot()) invariant l.ImmutableState() == old(l.ImmutableState()) + decreases len(terms) - i for i := 0; i < len(terms); i++ { snap1 := l.Snapshot() l.LabelCtx().IsPublishableMonotonic(snap, snap1, terms[i]) @@ -606,6 +634,7 @@ func MultiPublish(l *ll.LabeledLibrary, terms seq[tm.Term]) { // operation 6: participant corruption ghost +decreases requires l.Mem() ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) @@ -634,6 +663,7 @@ func CorruptParticipant(l *ll.LabeledLibrary, principal p.Principal) (arbTerm tm // operation 7: session corruption ghost +decreases requires l.Mem() ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) @@ -661,12 +691,13 @@ func CorruptSession(l *ll.LabeledLibrary, sessionId p.Id) (arbTerm tm.Term) { // operation 8: drop message ghost +decreases requires l.Mem() requires l.Snapshot().messageOccurs(idSender, idReceiver, msg) // only previously sent message can be dropped ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) ensures l.Snapshot().isMessageDroppedAt(idSender, idReceiver, msg) -func DropMessage(l *ll.LabeledLibrary, idSender, idReceiver p.Principal, msg tm.Term) { +func DropMessage(l *ll.LabeledLibrary, idSender, idReceiver p.Principal, ghost msg tm.Term) { msgBytes := lib.NewByteStringWithContent(tm.gamma(msg)) l.MessageOccursImpliesMessageInv(idSender, idReceiver, msg) unfold l.Mem() @@ -680,19 +711,21 @@ func DropMessage(l *ll.LabeledLibrary, idSender, idReceiver p.Principal, msg tm. // to its attacker knowledge (similarly to how the attacker adds a term derived by // function application to its knowledge) ghost +decreases requires l.Mem() ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) -ensures err == nil ==> att.attackerKnows(l.Snapshot(), msg) -func Recv(l *ll.LabeledLibrary, idSender, idReceiver p.Principal) (err error, msg tm.Term) { +ensures err == nil ==> att.attackerKnows(l.Snapshot(), msgT) +func Recv(l *ll.LabeledLibrary, idSender, idReceiver p.Principal) (err error, msgT tm.Term) { snapshot := l.Snapshot() unfold l.Mem() - _, err, msg = l.com.Receive(idSender, idReceiver, snapshot) + var msg lib.ByteString + msg, err, msgT = l.com.AttackerReceive(idSender, idReceiver, snapshot) fold l.Mem() ghost if err == nil { - prev := l.MessageOccursImpliesMessageInv(idSender, idReceiver, msg) + prev := l.MessageOccursImpliesMessageInv(idSender, idReceiver, msgT) (tr.getPrev(prev)).isSuffixTransitive(prev, l.Snapshot()) - tri.messageInvTransitive(l.Ctx(), idSender, idReceiver, msg, tr.getPrev(prev), l.Snapshot()) - l.Publish(msg) + tri.messageInvTransitive(l.Ctx(), idSender, idReceiver, msgT, tr.getPrev(prev), l.Snapshot()) + l.Publish(msgT) } } diff --git a/concurrentdatastructure/concurrent-datastructure.gobra b/concurrentdatastructure/concurrent-datastructure.gobra index 568bb51..897f139 100644 --- a/concurrentdatastructure/concurrent-datastructure.gobra +++ b/concurrentdatastructure/concurrent-datastructure.gobra @@ -1,39 +1,38 @@ package concurrentdatastructure -import "sync" import arb "github.com/ModularVerification/ReusableVerificationLibrary/arbitrary" import p "github.com/ModularVerification/ReusableVerificationLibrary/principal" import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" -type ClientId = p.Id -type ValueType = tr.TraceEntry +ghost type ClientId = p.Id +ghost type ValueType = tr.TraceEntry -type ClientHistoryMutex struct { - mutex *sync.Mutex - /** each client has a last seen value */ - snapshots map[ClientId]*ValueType - currentValue *ValueType +ghost type ClientHistoryMutex ghost struct { + mutex gpointer[GhostMutex] + /** each client has a snapshot */ + snapshots dict[ClientId]gpointer[ValueType] + currentValue gpointer[ValueType] } -pred (m *ClientHistoryMutex) ClientHistoryMutexStateInit() { +pred (m gpointer[ClientHistoryMutex]) ClientHistoryMutexStateInit() { acc(m) && - acc(m.mutex) && *m.mutex == sync.Mutex{} && - acc(m.snapshots) && len(m.snapshots) == 0 && + acc(m.mutex) && *m.mutex == GhostMutex{} && + len(m.snapshots) == 0 && acc(m.currentValue) } -pred (m *ClientHistoryMutex) ClientHistoryMutexStateInitWithInv(inv ClientHistoryInv, ghost clients set[ClientId]) { - acc(m) && acc(m.snapshots) && +pred (m gpointer[ClientHistoryMutex]) ClientHistoryMutexStateInitWithInv(inv ClientHistoryInv, ghost clients set[ClientId]) { + acc(m) && acc(m.mutex.LockP(), _) && m.mutex.LockInv() == ClientHistoryMutexInv! && clients == domain(m.snapshots) && (forall client1, client2 ClientId :: client1 in domain(m.snapshots) && client2 in domain(m.snapshots) && client1 != client2 ==> (m.snapshots)[client1] != (m.snapshots)[client2]) && - (forall snapshot *ValueType :: snapshot in range(m.snapshots) ==> acc(snapshot, 1/2)) + (forall snapshot gpointer[ValueType] :: snapshot in range(m.snapshots) ==> acc(snapshot, 1/2)) } /** represents the state in the mutex's unlocked state */ -pred (m *ClientHistoryMutex) ClientHistoryMutexState(inv ClientHistoryInv, client ClientId) { +pred (m gpointer[ClientHistoryMutex]) ClientHistoryMutexState(inv ClientHistoryInv, client ClientId) { // the idea is that each client get 1/len(clients) many permissions - acc(m, _) && acc(m.snapshots, _) && inv != nil && + acc(m, _) && inv != nil && acc(m.mutex.LockP(), _) && m.mutex.LockInv() == ClientHistoryMutexInv! && client in domain(m.snapshots) && // remaining 1/2 permission to value in snapshot belonging to current client: @@ -41,9 +40,9 @@ pred (m *ClientHistoryMutex) ClientHistoryMutexState(inv ClientHistoryInv, clien } /** represents the state in the mutex's locked state */ -pred (m *ClientHistoryMutex) ClientHistoryMutexStateLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) { +pred (m gpointer[ClientHistoryMutex]) ClientHistoryMutexStateLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) { // beginning copy of clientHistoryMutexState - acc(m, _) && acc(m.snapshots, _) && inv != nil && + acc(m, _) && inv != nil && acc(m.mutex.LockP(), _) && m.mutex.LockInv() == ClientHistoryMutexInv! && client in domain(m.snapshots) && // remaining 1/2 permission to value in snapshot belonging to current client: @@ -52,72 +51,75 @@ pred (m *ClientHistoryMutex) ClientHistoryMutexStateLocked(inv ClientHistoryInv, m.mutex.UnlockP() && acc(m.currentValue) && *m.currentValue == currentValue && - (forall snapshot *ValueType :: { inv.TwoStepValueInv(*snapshot, *m.currentValue) } snapshot in range(m.snapshots) ==> acc(snapshot, 1/2) && inv.TwoStepValueInv(*snapshot, *m.currentValue)) + (forall snapshot gpointer[ValueType] :: { inv.TwoStepValueInv(*snapshot, *m.currentValue) } snapshot in range(m.snapshots) ==> acc(snapshot, 1/2) && inv.TwoStepValueInv(*snapshot, *m.currentValue)) } /** represents the invariant that is associated with the mutex */ -pred ClientHistoryMutexInv(inv ClientHistoryInv, currentValue *ValueType, ghost snapshots set[*ValueType]) { +pred ClientHistoryMutexInv(inv ClientHistoryInv, currentValue gpointer[ValueType], ghost snapshots set[gpointer[ValueType]]) { inv != nil && acc(currentValue) && inv.CurrentValueInv(*currentValue) && - (forall snapshot *ValueType :: { inv.TwoStepValueInv(*snapshot, *currentValue) } snapshot in snapshots ==> + (forall snapshot gpointer[ValueType] :: { inv.TwoStepValueInv(*snapshot, *currentValue) } snapshot in snapshots ==> acc(snapshot, 1/2) && inv.TwoStepValueInv(*snapshot, *currentValue)) } type ClientHistoryInv interface { /** invariant to specify properties that hold for the current value */ - pred CurrentValueInv(value ValueType) + pred CurrentValueInv(ghost value ValueType) /** two step invariant */ ghost decreases - pure TwoStepValueInv(oldValue ValueType, currentValue ValueType) bool + pure TwoStepValueInv(ghost oldValue ValueType, ghost currentValue ValueType) bool /** proof obligation to show that the two step invariant is reflexive */ ghost decreases ensures TwoStepValueInv(value, value) - TwoStepValueInvReflexive(value ValueType) + TwoStepValueInvReflexive(ghost value ValueType) /** proof obligation to show that the two step invariant is transitive */ ghost decreases requires TwoStepValueInv(val1, val2) && TwoStepValueInv(val2, val3) ensures TwoStepValueInv(val1, val3) - TwoStepValueInvTransitive(val1, val2, val3 ValueType) + TwoStepValueInvTransitive(ghost val1, val2, val3 ValueType) } // indirection for ClientHistoryInv that gives us the property that // `inv` is non-nil +ghost decreases requires acc(m.ClientHistoryMutexStateLocked(inv, client, currentValue), _) ensures inv != nil -pure func (m *ClientHistoryMutex) GetInvLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) ClientHistoryInv { +pure func (m gpointer[ClientHistoryMutex]) GetInvLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) ClientHistoryInv { return unfolding acc(m.ClientHistoryMutexStateLocked(inv, client, currentValue), _) in inv } +ghost decreases requires acc(m.ClientHistoryMutexState(inv, client), _) -pure func (m *ClientHistoryMutex) LastSeenValue(inv ClientHistoryInv, client ClientId) ValueType { +pure func (m gpointer[ClientHistoryMutex]) LastSeenValue(inv ClientHistoryInv, client ClientId) ValueType { return unfolding acc(m.ClientHistoryMutexState(inv, client), _) in *(m.snapshots)[client] } +ghost decreases requires acc(m.ClientHistoryMutexStateLocked(inv, client, currentValue), _) -pure func (m *ClientHistoryMutex) LastSeenValueLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) ValueType { +pure func (m gpointer[ClientHistoryMutex]) LastSeenValueLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) ValueType { return unfolding acc(m.ClientHistoryMutexStateLocked(inv, client, currentValue), _) in *(m.snapshots)[client] } ghost decreases requires acc(m.ClientHistoryMutexState(inv, client), _) -pure func (m *ClientHistoryMutex) Clients(inv ClientHistoryInv, client ClientId) set[ClientId] { +pure func (m gpointer[ClientHistoryMutex]) Clients(inv ClientHistoryInv, client ClientId) set[ClientId] { return unfolding acc(m.ClientHistoryMutexState(inv, client), _) in domain(m.snapshots) } ghost decreases requires acc(m.ClientHistoryMutexStateLocked(inv, client, currentValue), _) -pure func (m *ClientHistoryMutex) ClientsLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) set[ClientId] { +pure func (m gpointer[ClientHistoryMutex]) ClientsLocked(inv ClientHistoryInv, client ClientId, currentValue ValueType) set[ClientId] { return unfolding acc(m.ClientHistoryMutexStateLocked(inv, client, currentValue), _) in domain(m.snapshots) } @@ -128,7 +130,7 @@ requires acc(m.ClientHistoryMutexState(inv, client2), 1/16) ensures acc(m.ClientHistoryMutexState(inv, client1), 1/16) ensures acc(m.ClientHistoryMutexState(inv, client2), 1/16) ensures m.Clients(inv, client1) == m.Clients(inv, client2) -func (m *ClientHistoryMutex) ClientsAreIdentical(inv ClientHistoryInv, client1, client2 ClientId) { +func (m gpointer[ClientHistoryMutex]) ClientsAreIdentical(inv ClientHistoryInv, client1, client2 ClientId) { assert unfolding acc(m.ClientHistoryMutexState(inv, client1), 1/16) in unfolding acc(m.ClientHistoryMutexState(inv, client2), 1/16) in true } @@ -139,55 +141,47 @@ requires acc(m.ClientHistoryMutexState(inv, client2), 1/16) ensures acc(m.ClientHistoryMutexStateLocked(inv, client1, currentValue1), 1/16) ensures acc(m.ClientHistoryMutexState(inv, client2), 1/16) ensures m.ClientsLocked(inv, client1, currentValue1) == m.Clients(inv, client2) -func (m *ClientHistoryMutex) ClientsAreIdenticalLocked1(inv ClientHistoryInv, client1, client2 ClientId, currentValue1 ValueType) { +func (m gpointer[ClientHistoryMutex]) ClientsAreIdenticalLocked1(inv ClientHistoryInv, client1, client2 ClientId, currentValue1 ValueType) { assert unfolding acc(m.ClientHistoryMutexStateLocked(inv, client1, currentValue1), 1/16) in unfolding acc(m.ClientHistoryMutexState(inv, client2), 1/16) in true } +ghost decreases ensures m.ClientHistoryMutexStateInit() -func NewClientHistoryMutex() (m *ClientHistoryMutex) { +func NewClientHistoryMutex() (m gpointer[ClientHistoryMutex]) { m = &ClientHistoryMutex{} - m.mutex = &sync.Mutex{} + m.mutex = &GhostMutex{} var value@ ValueType m.currentValue = &value - m.snapshots = make(map[ClientId]*ValueType) + m.snapshots = dict[ClientId]gpointer[ValueType]{} fold m.ClientHistoryMutexStateInit() } +ghost decreases requires m.ClientHistoryMutexStateInit() requires inv != nil && isComparable(inv) requires noPerm < p && p <= writePerm requires 0 < len(clients) -requires forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> acc(&clients[j], p) requires forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] requires inv.CurrentValueInv(initVal) -ensures forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> acc(&clients[j], p) ensures forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] ensures forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> m.ClientHistoryMutexState(inv, clients[j]) ensures forall j, k int :: { clients[j], clients[k] } 0 <= j && j < len(clients) && 0 <= k && k < len(clients) ==> clients[k] in m.Clients(inv, clients[j]) -func (m *ClientHistoryMutex) SetInv(inv ClientHistoryInv, clients []ClientId, initVal ValueType, ghost p perm) { +func (m gpointer[ClientHistoryMutex]) SetInv(inv ClientHistoryInv, clients seq[ClientId], initVal ValueType, p perm) { unfold m.ClientHistoryMutexStateInit() - - /** sequence representation of clients */ - clientSeq := seq[ClientId]{} invariant 0 <= i && i <= len(clients) // we have permissions to m, its fields, and the clients (which are pairwise disjoint): - invariant acc(m, 1/2) && acc(m.snapshots) - invariant forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> acc(&clients[j], p) + invariant acc(m, 1/2) && acc(&m.snapshots, 1/2) invariant forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] - // clientSeq becomes more and more an abstraction of `clients`: - invariant len(clientSeq) == i - invariant forall j int :: { clientSeq[j] } 0 <= j && j < i ==> clients[j] == clientSeq[j] - invariant domain(m.snapshots) == set(clientSeq) + invariant domain(m.snapshots) == set(clients[:i]) // each client has its own snapshot pointer and each snapshot satisfies the invariant: - invariant forall snapshot *ValueType :: { inv.TwoStepValueInv(*snapshot, initVal) } snapshot in range(m.snapshots) ==> acc(snapshot) && inv.TwoStepValueInv(*snapshot, initVal) + invariant forall snapshot gpointer[ValueType] :: { inv.TwoStepValueInv(*snapshot, initVal) } snapshot in range(m.snapshots) ==> acc(snapshot) && inv.TwoStepValueInv(*snapshot, initVal) invariant forall client1, client2 ClientId :: { (m.snapshots)[client1], (m.snapshots)[client2] } client1 in domain(m.snapshots) && client2 in domain(m.snapshots) && client1 != client2 ==> (m.snapshots)[client1] != (m.snapshots)[client2] decreases len(clients) - i for i := 0; i < len(clients); i++ { client := clients[i] - clientSeq = clientSeq ++ seq[ClientId]{ client } clientValue@ := initVal length := len(m.snapshots) assert !(client in domain(m.snapshots)) @@ -200,10 +194,8 @@ func (m *ClientHistoryMutex) SetInv(inv ClientHistoryInv, clients []ClientId, in fold ClientHistoryMutexInv!() m.mutex.SetInv(ClientHistoryMutexInv!) - fold m.ClientHistoryMutexStateInitWithInv(inv, set(clientSeq)) - m.split(inv, clientSeq) - // the following assert stmt is necessary: - assert forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> clients[j] == clientSeq[j] + fold m.ClientHistoryMutexStateInitWithInv(inv, set(clients)) + m.split(inv, clients) } ghost @@ -213,7 +205,7 @@ requires forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < le requires m.ClientHistoryMutexStateInitWithInv(inv, set(clients)) ensures forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> m.ClientHistoryMutexState(inv, clients[j]) ensures forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> set(clients) subset m.Clients(inv, clients[j]) -func (m *ClientHistoryMutex) split(inv ClientHistoryInv, ghost clients seq[ClientId]) { +func (m gpointer[ClientHistoryMutex]) split(inv ClientHistoryInv, ghost clients seq[ClientId]) { unfold m.ClientHistoryMutexStateInitWithInv(inv, set(clients)) // some abbreviations for the following loop: @@ -224,7 +216,6 @@ func (m *ClientHistoryMutex) split(inv ClientHistoryInv, ghost clients seq[Clien invariant forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] invariant acc(m, _) invariant m.currentValue == currentValue && m.mutex == mutex - invariant acc(m.snapshots, _) invariant acc(mutex.LockP(), _) && mutex.LockInv() == ClientHistoryMutexInv!; invariant forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> clients[j] in domain(m.snapshots) invariant forall client1, client2 ClientId :: { (m.snapshots)[client1], (m.snapshots)[client2] } client1 in domain(m.snapshots) && client2 in domain(m.snapshots) && client1 != client2 ==> (m.snapshots)[client1] != (m.snapshots)[client2] @@ -239,8 +230,8 @@ func (m *ClientHistoryMutex) split(inv ClientHistoryInv, ghost clients seq[Clien } } -// TODO prove termination. This is currently not possible because we cannot show -// that `Lock` eventually succeeds. +ghost +// we assume termination and atomicity of this ghost lock decreases _ requires m.ClientHistoryMutexState(inv, client) ensures m.ClientHistoryMutexStateLocked(inv, client, currentValue) && inv != nil @@ -249,7 +240,7 @@ ensures inv.CurrentValueInv(currentValue) // LastSeenValue remains unchanged: ensures m.LastSeenValueLocked(inv, client, currentValue) == old(m.LastSeenValue(inv, client)) ensures m.ClientsLocked(inv, client, currentValue) == old(m.Clients(inv, client)) -func (m *ClientHistoryMutex) Lock(inv ClientHistoryInv, client ClientId) (currentValue ValueType) { +func (m gpointer[ClientHistoryMutex]) Lock(inv ClientHistoryInv, client ClientId) (currentValue ValueType) { unfold m.ClientHistoryMutexState(inv, client) m.mutex.Lock() unfold ClientHistoryMutexInv!() @@ -268,7 +259,7 @@ requires inv.CurrentValueInv(newValue) ensures m.ClientHistoryMutexState(inv, client) ensures unfolding m.ClientHistoryMutexState(inv, client) in *(m.snapshots)[client] == newValue ensures m.Clients(inv, client) == old(m.ClientsLocked(inv, client, currentValue)) -func (m *ClientHistoryMutex) Unlock(inv ClientHistoryInv, client ClientId, currentValue, newValue ValueType) { +func (m gpointer[ClientHistoryMutex]) Unlock(inv ClientHistoryInv, client ClientId, currentValue, newValue ValueType) { inv.TwoStepValueInvReflexive(newValue) m.UnlockWithSnapshot(inv, client, currentValue, newValue, newValue) } @@ -289,10 +280,11 @@ ensures m.Clients(inv, client) == old(m.ClientsLocked(inv, client, currentValue * similar to `Unlock` in the sense that the lock is released. * however, this method allows to manually specify the snapshot to which this client's lastSeenValue should be set */ -func (m *ClientHistoryMutex) UnlockWithSnapshot(inv ClientHistoryInv, client ClientId, currentValue, newValue, snapshot ValueType) { +func (m gpointer[ClientHistoryMutex]) UnlockWithSnapshot(inv ClientHistoryInv, client ClientId, currentValue, newValue, snapshot ValueType) { unfold m.ClientHistoryMutexStateLocked(inv, client, currentValue) m.applyInvTransitivity(inv, range(m.snapshots), currentValue, newValue, 1/2) - *(m.snapshots)[client] = snapshot + snapshotPtr := (m.snapshots)[client] + *snapshotPtr = snapshot // the following assert statement is necessary due to an incompleteness: assert *(m.snapshots)[client] == snapshot *m.currentValue = newValue @@ -305,12 +297,12 @@ ghost decreases requires noPerm < p && p <= writePerm requires inv != nil -requires forall snapshot *ValueType :: { inv.TwoStepValueInv(*snapshot, currentValue) } snapshot in snapshots ==> +requires forall snapshot gpointer[ValueType] :: { inv.TwoStepValueInv(*snapshot, currentValue) } snapshot in snapshots ==> acc(snapshot, p) && inv.TwoStepValueInv(*snapshot, currentValue) requires inv.TwoStepValueInv(currentValue, newValue) -ensures forall snapshot *ValueType :: { inv.TwoStepValueInv(*snapshot, newValue) } snapshot in snapshots ==> +ensures forall snapshot gpointer[ValueType] :: { inv.TwoStepValueInv(*snapshot, newValue) } snapshot in snapshots ==> acc(snapshot, p) && inv.TwoStepValueInv(*snapshot, newValue) -func (m *ClientHistoryMutex) applyInvTransitivity(inv ClientHistoryInv, snapshots set[*ValueType], currentValue, newValue ValueType, p perm) { +func (m gpointer[ClientHistoryMutex]) applyInvTransitivity(inv ClientHistoryInv, snapshots set[gpointer[ValueType]], currentValue, newValue ValueType, p perm) { // non-deterministically choose a snapshot arbitrarySnapshot@ := arb.GetArbTraceEntry() if &arbitrarySnapshot in snapshots { @@ -320,7 +312,7 @@ func (m *ClientHistoryMutex) applyInvTransitivity(inv ClientHistoryInv, snapshot // forall introduction: assert &arbitrarySnapshot in snapshots ==> inv.TwoStepValueInv(arbitrarySnapshot, newValue) - assume forall snapshot *ValueType :: { inv.TwoStepValueInv(*snapshot, newValue) } snapshot in snapshots ==> + assume forall snapshot gpointer[ValueType] :: { inv.TwoStepValueInv(*snapshot, newValue) } snapshot in snapshots ==> inv.TwoStepValueInv(*snapshot, newValue) } @@ -331,6 +323,6 @@ requires inv != nil requires acc(snapshot, p) && inv.TwoStepValueInv(*snapshot, currentValue) requires inv.TwoStepValueInv(currentValue, newValue) ensures acc(snapshot, p) && inv.TwoStepValueInv(*snapshot, newValue) -func (m *ClientHistoryMutex) applyInvTransitivitySingle(inv ClientHistoryInv, snapshot *ValueType, currentValue, newValue ValueType, p perm) { +func (m gpointer[ClientHistoryMutex]) applyInvTransitivitySingle(inv ClientHistoryInv, snapshot gpointer[ValueType], currentValue, newValue ValueType, p perm) { inv.TwoStepValueInvTransitive(*snapshot, currentValue, newValue) } diff --git a/concurrentdatastructure/ghost-mutex.gobra b/concurrentdatastructure/ghost-mutex.gobra new file mode 100644 index 0000000..3564fc4 --- /dev/null +++ b/concurrentdatastructure/ghost-mutex.gobra @@ -0,0 +1,36 @@ +// Copyright 2009 The Go Authors. All rights reserved. +// Use of this source code is governed by a BSD-style +// license that can be found in https://golang.org/LICENSE + +package concurrentdatastructure + +type GhostMutex struct { + state int32 + stema uint32 +} + +pred (m gpointer[GhostMutex]) LockP() +pred (m gpointer[GhostMutex]) UnlockP() + +ghost +requires acc(m.LockP(), _) +decreases _ +pure func (m gpointer[GhostMutex]) LockInv() pred() + +ghost +requires inv() && acc(m) && *m == GhostMutex{} +ensures m.LockP() && m.LockInv() == inv +decreases +func (m gpointer[GhostMutex]) SetInv(ghost inv pred()) + +ghost +requires acc(m.LockP(), _) +ensures m.LockP() && m.UnlockP() && m.LockInv()() +decreases // we assume that the ghost lock is justified via atomicity of critical sections. Thus, `Lock` will eventually return +func (m gpointer[GhostMutex]) Lock() + +ghost +requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()() +ensures m.LockP() +decreases +func (m gpointer[GhostMutex]) Unlock() diff --git a/event/event.gobra b/event/event.gobra index b457d9c..500c67e 100644 --- a/event/event.gobra +++ b/event/event.gobra @@ -7,7 +7,7 @@ package event type EventParams interface {} type EventType int -type Event struct { +ghost type Event ghost struct { typ EventType params EventParams } diff --git a/label/secrecy-label.gobra b/label/secrecy-label.gobra index ac10c6d..c6060da 100644 --- a/label/secrecy-label.gobra +++ b/label/secrecy-label.gobra @@ -2,7 +2,7 @@ package label import p "github.com/ModularVerification/ReusableVerificationLibrary/principal" -type SecrecyLabel domain { +ghost type SecrecyLabel domain { // constructors // type 0 func Public() SecrecyLabel diff --git a/labeledlibrary/channelcommunication/channel-communication.go b/labeledlibrary/channelcommunication/channel-communication.go index 6bcebc5..ed3d0e4 100644 --- a/labeledlibrary/channelcommunication/channel-communication.go +++ b/labeledlibrary/channelcommunication/channel-communication.go @@ -1,15 +1,18 @@ package channelcommunication //@ import ll "github.com/ModularVerification/ReusableVerificationLibrary/labeledlibrary" -import lib "github.com/ModularVerification/ReusableVerificationLibrary/labeledlibrary/library" -import p "github.com/ModularVerification/ReusableVerificationLibrary/principal" +import ( + lib "github.com/ModularVerification/ReusableVerificationLibrary/labeledlibrary/library" + p "github.com/ModularVerification/ReusableVerificationLibrary/principal" +) + //@ import tm "github.com/ModularVerification/ReusableVerificationLibrary/term" //@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" - type ChannelCommunicaton struct { channels map[ChannelKey]chan []byte } + // the following statement is not necessary but makes subtyping explicit (for documentation purposes) //@ (* ChannelCommunicaton) implements ll.Communication @@ -49,6 +52,27 @@ func (com *ChannelCommunicaton) Send(idSender, idReceiver p.Principal, msg lib.B return nil } +/*@ +ghost +trusted +decreases +requires acc(com.LibMem(), 1/16) +requires acc(lib.Mem(msg), 1/16) +requires lib.Abs(msg) == tm.gamma(msgT) +requires snapshot.isMessageAt(idSender, idReceiver, msgT) +ensures acc(com.LibMem(), 1/16) +ensures acc(lib.Mem(msg), 1/16) +func (com *ChannelCommunicaton) AttackerSend(idSender, idReceiver p.Principal, msg lib.ByteString, msgT tm.Term, snapshot tr.TraceEntry) error { + channel := (com.channels)[ChannelKey{idSender, idReceiver}] + if len(ch) == cap(ch) { + // channel is full + return lib.AttackerNewError("Channel is full, send would block") + } + channel <- msg + return nil +} +@*/ + //@ trusted //@ requires acc(com.LibMem(), 1/16) //@ ensures acc(com.LibMem(), 1/16) @@ -60,3 +84,23 @@ func (com *ChannelCommunicaton) Receive(idSender, idReceiver p.Principal /*@, gh msg = <-channel return msg, nil /*@, tm.oneTerm(msg) @*/ } + +/*@ +ghost +trusted +decreases +requires acc(com.LibMem(), 1/16) +ensures acc(com.LibMem(), 1/16) +ensures err == nil ==> lib.Mem(msg) +ensures err == nil ==> lib.Abs(msg) == tm.gamma(msgT) +ensures err == nil ==> snapshot.messageOccurs(idSender, idReceiver, msgT) +func (com *ChannelCommunicaton) AttackerReceive(idSender, idReceiver p.Principal, ghost snapshot tr.TraceEntry) (msg lib.ByteString, err error, ghost msgT tm.Term) { + channel := (com.channels)[ChannelKey{idSender, idReceiver}] + if len(ch) == 0 { + err = lib.AttackerNewError("Channel is empty, receive would block") + return + } + msg = <-channel + return msg, nil, tm.oneTerm(msg) +} +@*/ diff --git a/labeledlibrary/crypto.go b/labeledlibrary/crypto.go index 13df0bd..9b3940b 100644 --- a/labeledlibrary/crypto.go +++ b/labeledlibrary/crypto.go @@ -21,9 +21,9 @@ import ( //@ ensures err == nil ==> lib.Abs(nonce) == tm.gamma(tm.random(lib.Abs(nonce), nonceLabel, u.Nonce(usageString))) //@ ensures err == nil ==> l.Snapshot().isNonceAt(tm.random(lib.Abs(nonce), nonceLabel, u.Nonce(usageString))) //@ ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> (l.LabelCtx()).NonceForEventIsUnique(tm.random(lib.Abs(nonce), nonceLabel, u.Nonce(usageString)), eventType) -func (l *LabeledLibrary) CreateNonce(/*@ ghost nonceLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/) (nonce lib.ByteString, err error) { +func (l *LabeledLibrary) CreateNonce( /*@ ghost nonceLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/ ) (nonce lib.ByteString, err error) { //@ unfold l.Mem() - nonce, err = l.s.CreateNonce(/*@ tri.GetLabeling(l.ctx), nonceLabel, usageString, eventTypes @*/) + nonce, err = l.s.CreateNonce( /*@ tri.GetLabeling(l.ctx), nonceLabel, usageString, eventTypes @*/ ) // store nonce on trace /*@ ghost if err == nil { @@ -44,12 +44,11 @@ func (l *LabeledLibrary) CreateNonce(/*@ ghost nonceLabel label.SecrecyLabel, gh //@ ensures err == nil ==> lib.Abs(sk) == tm.gamma(skT) && lib.Abs(pk) == tm.createPkB(lib.Abs(sk)) //@ ensures err == nil ==> l.Snapshot().isNonceAt(skT) //@ ensures err == nil ==> skT == tm.random(lib.Abs(sk), label.Readers(set[p.Id]{ l.OwnerWoThread() }), u.PkeKey(usageString)) -// TODO make skT ghost -func (l *LabeledLibrary) GeneratePkeKey(/*@ ghost usageString string @*/) (pk, sk lib.ByteString, err error /*@, skT tm.Term @*/) { +func (l *LabeledLibrary) GeneratePkeKey( /*@ ghost usageString string @*/ ) (pk, sk lib.ByteString, err error /*@, ghost skT tm.Term @*/) { //@ ownerWoThread := l.OwnerWoThread() //@ unfold l.Mem() //@ keyLabel := label.Readers(set[p.Id]{ ownerWoThread }) - pk, sk, err = l.s.GeneratePkeKey(/*@ tri.GetLabeling(l.ctx), keyLabel, usageString, set[ev.EventType]{} @*/) + pk, sk, err = l.s.GeneratePkeKey( /*@ tri.GetLabeling(l.ctx), keyLabel, usageString, set[ev.EventType]{} @*/ ) // store sk on trace /*@ ghost if err == nil { @@ -71,11 +70,11 @@ func (l *LabeledLibrary) GeneratePkeKey(/*@ ghost usageString string @*/) (pk, s //@ ensures err == nil ==> skT == tm.random(lib.Abs(key), label.Readers(set[p.Id]{ l.OwnerWoThread() }), u.DhKey(usageString)) //@ ensures err == nil ==> l.Snapshot().isNonceAt(skT) //@ ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> l.LabelCtx().NonceForEventIsUnique(skT, eventType) -func (l *LabeledLibrary) GenerateDHKey(/*@ ghost usageString string, ghost eventTypes set[ev.EventType] @*/) (key lib.ByteString, err error /*@, ghost skT tm.Term @*/) { +func (l *LabeledLibrary) GenerateDHKey( /*@ ghost usageString string, ghost eventTypes set[ev.EventType] @*/ ) (key lib.ByteString, err error /*@, ghost skT tm.Term @*/) { //@ ownerWoThread := l.OwnerWoThread() //@ unfold l.Mem() //@ keyLabel := label.Readers(set[p.Id]{ ownerWoThread }) - key, err = l.s.GenerateDHKey(/*@ tri.GetLabeling(l.ctx), keyLabel, usageString, eventTypes @*/) + key, err = l.s.GenerateDHKey( /*@ tri.GetLabeling(l.ctx), keyLabel, usageString, eventTypes @*/ ) // store key on trace /*@ ghost if err == nil { @@ -97,12 +96,11 @@ func (l *LabeledLibrary) GenerateDHKey(/*@ ghost usageString string, ghost event //@ ensures err == nil ==> lib.Abs(sk) == tm.gamma(skT) && lib.Abs(pk) == tm.createPkB(lib.Abs(sk)) //@ ensures err == nil ==> l.Snapshot().isNonceAt(skT) //@ ensures err == nil ==> skT == tm.random(lib.Abs(sk), label.Readers(set[p.Id]{ l.OwnerWoThread() }), u.SigningKey(usageString)) -// TODO make skT ghost -func (l *LabeledLibrary) GenerateSigningKey(/*@ ghost usageString string @*/) (pk, sk lib.ByteString, err error /*@, skT tm.Term @*/) { +func (l *LabeledLibrary) GenerateSigningKey( /*@ ghost usageString string @*/ ) (pk, sk lib.ByteString, err error /*@, ghost skT tm.Term @*/) { //@ ownerWoThread := l.OwnerWoThread() //@ unfold l.Mem() //@ keyLabel := label.Readers(set[p.Id]{ ownerWoThread }) - pk, sk, err = l.s.GenerateSigningKey(/*@ tri.GetLabeling(l.ctx), keyLabel, usageString, set[ev.EventType]{} @*/) + pk, sk, err = l.s.GenerateSigningKey( /*@ tri.GetLabeling(l.ctx), keyLabel, usageString, set[ev.EventType]{} @*/ ) // store sk on trace /*@ ghost if err == nil { @@ -137,6 +135,32 @@ func (l *LabeledLibrary) Enc(msg, pk lib.ByteString /*@, ghost msgT tm.Term, gho return } +/*@ +ghost +decreases +requires l.Mem() +requires acc(lib.Mem(msg), 1/8) +requires lib.Abs(msg) == tm.gamma(msgT) +requires acc(lib.Mem(pk), 1/8) +requires lib.Abs(pk) == tm.gamma(pkT) +requires l.LabelCtx().CanEncrypt(l.Snapshot(), msgT, pkT) || (l.LabelCtx().IsPublishable(l.Snapshot(), msgT) && l.LabelCtx().IsPublishable(l.Snapshot(), pkT)) +ensures l.Mem() +ensures l.ImmutableState() == old(l.ImmutableState()) +ensures l.Snapshot() == old(l.Snapshot()) +ensures acc(lib.Mem(msg), 1/8) +ensures acc(lib.Mem(pk), 1/8) +ensures err == nil ==> lib.Mem(ciphertext) +ensures err == nil ==> lib.Abs(ciphertext) == tm.encryptB(lib.Abs(msg), lib.Abs(pk)) +ensures err == nil ==> l.LabelCtx().IsPublishable(l.Snapshot(), tm.encrypt(msgT, pkT)) +func (l *LabeledLibrary) AttackerEnc(msg, pk lib.ByteString, msgT tm.Term, pkT tm.Term) (ciphertext lib.ByteString, err error) { + unfold l.Mem() + ciphertext, err = l.s.AttackerEnc(msg, pk) + fold l.Mem() + l.LabelCtx().CiphertextIsPublishable(l.Snapshot(), msgT, pkT) + return +} +@*/ + //@ requires l.Mem() //@ requires acc(lib.Mem(ciphertext), 1/8) //@ requires lib.Abs(ciphertext) == tm.gamma(ciphertextT) @@ -174,6 +198,44 @@ func (l *LabeledLibrary) Dec(ciphertext, sk lib.ByteString /*@, ghost ciphertext return } +/*@ +ghost +decreases +requires l.Mem() +requires acc(lib.Mem(ciphertext), 1/8) +requires lib.Abs(ciphertext) == tm.gamma(ciphertextT) +requires acc(lib.Mem(sk), 1/8) +requires lib.Abs(sk) == tm.gamma(skT) +requires l.LabelCtx().CanDecrypt(l.Snapshot(), ciphertextT, skT, skOwner) +ensures l.Mem() +ensures l.ImmutableState() == old(l.ImmutableState()) +ensures l.Snapshot() == old(l.Snapshot()) +ensures acc(lib.Mem(ciphertext), 1/8) +ensures acc(lib.Mem(sk), 1/8) +ensures err == nil ==> lib.Mem(msg) +ensures err == nil ==> lib.Abs(ciphertext) == tm.encryptB(lib.Abs(msg), tm.createPkB(lib.Abs(sk))) +ensures err == nil ==> (forall msgT tm.Term :: { tm.encrypt(msgT, tm.createPk(skT)) } ciphertextT == tm.encrypt(msgT, tm.createPk(skT)) ==> + l.LabelCtx().WasDecrypted(l.Snapshot(), msgT, skT, skOwner)) +func (l *LabeledLibrary) AttackerDec(ciphertext, sk lib.ByteString, ciphertextT tm.Term, skT tm.Term, skOwner p.Id) (msg lib.ByteString, err error) { + unfold l.Mem() + msg, err = l.s.AttackerDec(ciphertext, sk) + fold l.Mem() + if err == nil { + pkT := tm.createPk(skT) + + // we choose an arbitrary msgT and then show that if we assume that it's the correct + // we can call `DecryptSatisfiesInvariant` which then gives us an implication with the given quantifier + arbMsgT := arb.GetArbTerm() + if ciphertextT == tm.encrypt(arbMsgT, pkT) { + l.LabelCtx().DecryptSatisfiesInvariant(l.Snapshot(), arbMsgT, skT, skOwner) + } + // forall introduction: + assert ciphertextT == tm.encrypt(arbMsgT, pkT) ==> l.LabelCtx().WasDecrypted(l.Snapshot(), arbMsgT, skT, skOwner) + assume forall msgT tm.Term :: { tm.encrypt(msgT, pkT) } ciphertextT == tm.encrypt(msgT, pkT) ==> l.LabelCtx().WasDecrypted(l.Snapshot(), msgT, skT, skOwner) + } + return +} + //@ requires l.Mem() //@ requires acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16) //@ requires lib.Size(key) == 32 && lib.Size(nonce) == 12 @@ -201,6 +263,37 @@ func (l *LabeledLibrary) AeadEnc(key, nonce, plaintext, additionalData lib.ByteS return } +/*@ +ghost +decreases +requires l.Mem() +requires acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16) +requires lib.Size(key) == 32 && lib.Size(nonce) == 12 +requires plaintext != nil ==> acc(lib.Mem(plaintext), 1/16) +requires additionalData != nil ==> acc(lib.Mem(additionalData), 1/16) +requires lib.Abs(key) == tm.gamma(keyT) +requires lib.Abs(nonce) == tm.gamma(nonceT) +requires lib.SafeAbs(plaintext, 0) == tm.gamma(plaintextT) +requires lib.SafeAbs(additionalData, 0) == tm.gamma(adT) +requires l.LabelCtx().CanAeadEncrypt(l.Snapshot(), keyT, nonceT, plaintextT, adT, keyL) || (l.LabelCtx().IsPublishable(l.Snapshot(), keyT) && l.LabelCtx().IsPublishable(l.Snapshot(), nonceT) && l.LabelCtx().IsPublishable(l.Snapshot(), plaintextT) && l.LabelCtx().IsPublishable(l.Snapshot(), adT)) +ensures l.Mem() +ensures l.ImmutableState() == old(l.ImmutableState()) +ensures l.Snapshot() == old(l.Snapshot()) +ensures acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16) +ensures plaintext != nil ==> acc(lib.Mem(plaintext), 1/16) +ensures additionalData != nil ==> acc(lib.Mem(additionalData), 1/16) +ensures err == nil ==> lib.Mem(ciphertext) && lib.Size(ciphertext) == (plaintext == nil ? 0 : lib.Size(plaintext)) + 16 +ensures err == nil ==> lib.Abs(ciphertext) == tm.aeadB(lib.Abs(key), lib.Abs(nonce), lib.SafeAbs(plaintext, 0), lib.SafeAbs(additionalData, 0)) +ensures err == nil ==> l.LabelCtx().IsPublishable(l.Snapshot(), tm.aead(keyT, nonceT, plaintextT, adT)) +func (l *LabeledLibrary) AttackerAeadEnc(key, nonce, plaintext, additionalData lib.ByteString, keyT tm.Term, nonceT tm.Term, plaintextT tm.Term, adT tm.Term, keyL label.SecrecyLabel) (ciphertext lib.ByteString, err error) { + unfold l.Mem() + ciphertext, err = l.s.AttackerAeadEnc(key, nonce, plaintext, additionalData) + fold l.Mem() + l.LabelCtx().AeadCiphertextIsPublishable(l.Snapshot(), keyT, nonceT, plaintextT, adT, keyL) + return +} +@*/ + //@ requires l.Mem() //@ requires acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16) //@ requires lib.Size(key) == 32 && lib.Size(nonce) == 12 @@ -240,6 +333,47 @@ func (l *LabeledLibrary) AeadDec(key, nonce, ciphertext, additionalData lib.Byte return } +/*@ +ghost +decreases +requires l.Mem() +requires acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16) +requires lib.Size(key) == 32 && lib.Size(nonce) == 12 +requires acc(lib.Mem(ciphertext), 1/16) +requires additionalData != nil ==> acc(lib.Mem(additionalData), 1/16) +requires lib.Abs(key) == tm.gamma(keyT) +requires lib.Abs(nonce) == tm.gamma(nonceT) +requires lib.Abs(ciphertext) == tm.gamma(ciphertextT) +requires lib.SafeAbs(additionalData, 0) == tm.gamma(adT) +requires l.LabelCtx().CanAeadDecrypt(l.Snapshot(), keyT, nonceT, ciphertextT, adT, keyL) +ensures l.Mem() +ensures l.ImmutableState() == old(l.ImmutableState()) +ensures l.Snapshot() == old(l.Snapshot()) +ensures acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16) && acc(lib.Mem(ciphertext), 1/16) +ensures additionalData != nil ==> acc(lib.Mem(additionalData), 1/16) +ensures err == nil ==> lib.Mem(res) && lib.Size(res) == lib.Size(ciphertext) - 16 +ensures err == nil ==> lib.Abs(ciphertext) == tm.aeadB(lib.Abs(key), lib.Abs(nonce), lib.Abs(res), lib.SafeAbs(additionalData, 0)) +ensures err == nil ==> (forall msgT tm.Term :: { tm.aead(keyT, nonceT, msgT, adT) } ciphertextT == tm.aead(keyT, nonceT, msgT, adT) ==> + l.LabelCtx().WasAeadDecrypted(l.Snapshot(), keyT, nonceT, msgT, adT, keyL)) +func (l *LabeledLibrary) AttackerAeadDec(key, nonce, ciphertext, additionalData lib.ByteString, keyT tm.Term, nonceT tm.Term, ciphertextT tm.Term, adT tm.Term, keyL label.SecrecyLabel) (res lib.ByteString, err error) { + unfold l.Mem() + res, err = l.s.AttackerAeadDec(key, nonce, ciphertext, additionalData) + fold l.Mem() + if err == nil { + // we choose an arbitrary msgT and then show that if we assume that it's the correct + // we can call `AeadDecryptSatisfiesInvariant` which then gives us an implication with the given quantifier + arbMsgT := arb.GetArbTerm() + if ciphertextT == tm.aead(keyT, nonceT, arbMsgT, adT) { + l.LabelCtx().AeadDecryptSatisfiesInvariant(l.Snapshot(), keyT, nonceT, arbMsgT, adT, keyL) + } + // forall introduction: + assert ciphertextT == tm.aead(keyT, nonceT, arbMsgT, adT) ==> l.LabelCtx().WasAeadDecrypted(l.Snapshot(), keyT, nonceT, arbMsgT, adT, keyL) + assume forall msgT tm.Term :: { tm.aead(keyT, nonceT, msgT, adT) } ciphertextT == tm.aead(keyT, nonceT, msgT, adT) ==> l.LabelCtx().WasAeadDecrypted(l.Snapshot(), keyT, nonceT, msgT, adT, keyL) + } + return +} +@*/ + //@ requires l.Mem() //@ requires acc(lib.Mem(msg), 1/8) //@ requires lib.Abs(msg) == tm.gamma(msgT) @@ -262,6 +396,32 @@ func (l *LabeledLibrary) Sign(msg, sk lib.ByteString /*@, ghost msgT tm.Term, gh return } +/*@ +ghost +decreases +requires l.Mem() +requires acc(lib.Mem(msg), 1/8) +requires lib.Abs(msg) == tm.gamma(msgT) +requires acc(lib.Mem(sk), 1/8) +requires lib.Abs(sk) == tm.gamma(skT) +requires l.LabelCtx().CanSign(l.Snapshot(), msgT, skT, skOwner) || (l.LabelCtx().IsPublishable(l.Snapshot(), msgT) && l.LabelCtx().IsPublishable(l.Snapshot(), skT)) +ensures l.Mem() +ensures l.ImmutableState() == old(l.ImmutableState()) +ensures l.Snapshot() == old(l.Snapshot()) +ensures acc(lib.Mem(msg), 1/8) +ensures acc(lib.Mem(sk), 1/8) +ensures err == nil ==> lib.Mem(signedMsg) +ensures err == nil ==> lib.Abs(signedMsg) == tm.signB(lib.Abs(msg), lib.Abs(sk)) +ensures err == nil ==> l.LabelCtx().IsPublishable(l.Snapshot(), tm.sign(msgT, skT)) +func (l *LabeledLibrary) AttackerSign(msg, sk lib.ByteString, msgT tm.Term, skT tm.Term, skOwner p.Id) (signedMsg lib.ByteString, err error) { + unfold l.Mem() + signedMsg, err = l.s.AttackerSign(msg, sk) + fold l.Mem() + l.LabelCtx().SignedMessageIsPublishable(l.Snapshot(), msgT, skT, skOwner) + return +} +@*/ + //@ requires l.Mem() //@ requires acc(lib.Mem(signedMsg), 1/8) //@ requires lib.Abs(signedMsg) == tm.gamma(signedMsgT) @@ -297,6 +457,43 @@ func (l *LabeledLibrary) Open(signedMsg, pk lib.ByteString /*@, ghost signedMsgT return } +/*@ +ghost +decreases +requires l.Mem() +requires acc(lib.Mem(signedMsg), 1/8) +requires lib.Abs(signedMsg) == tm.gamma(signedMsgT) +requires acc(lib.Mem(pk), 1/8) +requires lib.Abs(pk) == tm.gamma(tm.createPk(skT)) +requires l.LabelCtx().CanOpen(l.Snapshot(), signedMsgT, tm.createPk(skT), skOwner) +ensures l.Mem() +ensures l.ImmutableState() == old(l.ImmutableState()) +ensures l.Snapshot() == old(l.Snapshot()) +ensures acc(lib.Mem(signedMsg), 1/8) +ensures acc(lib.Mem(pk), 1/8) +ensures err == nil ==> lib.Mem(msg) +ensures err == nil ==> lib.Abs(signedMsg) == tm.signB(lib.Abs(msg), tm.gamma(skT)) +ensures err == nil ==> (forall msgT tm.Term :: { tm.sign(msgT, skT) } signedMsgT == tm.sign(msgT, skT) ==> + l.LabelCtx().WasOpened(l.Snapshot(), msgT, skT, skOwner)) +func (l *LabeledLibrary) AttackerOpen(signedMsg, pk lib.ByteString, signedMsgT tm.Term, skT tm.Term, skOwner p.Id) (msg lib.ByteString, err error) { + unfold l.Mem() + msg, err = l.s.AttackerOpen(signedMsg, pk, skT) + fold l.Mem() + if err == nil { + // we choose an arbitrary msgT and then show that if we assume that it's the correct + // we can call `OpenSatisfiesInvariant` which then gives us an implication with the given quantifier + arbMsgT := arb.GetArbTerm() + if signedMsgT == tm.sign(arbMsgT, skT) { + l.LabelCtx().OpenSatisfiesInvariant(l.Snapshot(), arbMsgT, skT, skOwner) + } + // forall introduction: + assert signedMsgT == tm.sign(arbMsgT, skT) ==> l.LabelCtx().WasOpened(l.Snapshot(), arbMsgT, skT, skOwner) + assume forall msgT tm.Term :: { tm.sign(msgT, skT) } signedMsgT == tm.sign(msgT, skT) ==> l.LabelCtx().WasOpened(l.Snapshot(), msgT, skT, skOwner) + } + return +} +@*/ + //@ requires l.Mem() //@ requires acc(lib.Mem(exp), 1/16) //@ requires lib.Abs(exp) == tm.gamma(expT) diff --git a/labeledlibrary/io.go b/labeledlibrary/io.go index 2f52f42..b1fc357 100644 --- a/labeledlibrary/io.go +++ b/labeledlibrary/io.go @@ -10,7 +10,6 @@ import ( //@ tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinvariant" ) - /** abstracts over different communication channels */ type Communication interface { //@ pred LibMem() @@ -23,18 +22,44 @@ type Communication interface { //@ ensures acc(lib.Mem(msg), 1/16) Send(idSender, idReceiver p.Principal, msg lib.ByteString /*@, ghost msgT tm.Term, ghost snapshot tr.TraceEntry @*/) error + /*@ + ghost + decreases + requires acc(LibMem(), 1/16) + requires acc(lib.Mem(msg), 1/16) + requires lib.Abs(msg) == tm.gamma(msgT) + requires snapshot.isMessageAt(idSender, idReceiver, msgT) + ensures acc(LibMem(), 1/16) + ensures acc(lib.Mem(msg), 1/16) + // Send operation that the attacker uses (for proving attacker completeness) + AttackerSend(idSender, idReceiver p.Principal, msg lib.ByteString, ghost msgT tm.Term, ghost snapshot tr.TraceEntry) error + @*/ + //@ requires acc(LibMem(), 1/16) //@ ensures acc(LibMem(), 1/16) //@ ensures err == nil ==> lib.Mem(msg) //@ ensures err == nil ==> lib.Abs(msg) == tm.gamma(msgT) //@ ensures err == nil ==> snapshot.messageOccurs(idSender, idReceiver, msgT) - // returns a message that was at or before `snapshot`. It's thus adviceable to synchronize to the globa + // returns a message that was at or before `snapshot`. It's thus adviceable to synchronize to the global // trace first such that the set of receivable messages is as big as possible Receive(idSender, idReceiver p.Principal /*@, ghost snapshot tr.TraceEntry @*/) (msg lib.ByteString, err error /*@, ghost msgT tm.Term @*/) -} + /*@ + ghost + decreases // we assume termination, i.e., this function returns an error if there are no messages that can be received + requires acc(LibMem(), 1/16) + ensures acc(LibMem(), 1/16) + ensures err == nil ==> lib.Mem(msg) + ensures err == nil ==> lib.Abs(msg) == tm.gamma(msgT) + ensures err == nil ==> snapshot.messageOccurs(idSender, idReceiver, msgT) + // returns a message that was at or before `snapshot`. It's thus adviceable to synchronize to the global + // trace first such that the set of receivable messages is as big as possible + // Receive operation that the attacker uses (for proving attacker completeness) + AttackerReceive(idSender, idReceiver p.Principal, ghost snapshot tr.TraceEntry) (msg lib.ByteString, err error, ghost msgT tm.Term) + @*/ +} -/** +/** * acts as a middleware between participant implementation and the library: * it not only delegates the call to the library but also creates a corresponding * trace trace @@ -86,6 +111,7 @@ func (l *LabeledLibrary) Receive(idSender, idReceiver p.Principal) (msg lib.Byte /*@ ghost +decreases requires l.Mem() requires (l.LabelCtx()).IsPublishable(l.Snapshot(), term) ensures l.Mem() diff --git a/labeledlibrary/library/crypto.go b/labeledlibrary/library/crypto.go index 5299778..d275bf6 100644 --- a/labeledlibrary/library/crypto.go +++ b/labeledlibrary/library/crypto.go @@ -3,14 +3,16 @@ package library import ( rand "crypto/rand" rsa "crypto/rsa" - x509 "crypto/x509" sha256 "crypto/sha256" - "errors" + x509 "crypto/x509" hex "encoding/hex" + "errors" + io "io" big "math/big" + chacha20poly1305 "golang.org/x/crypto/chacha20poly1305" sign "golang.org/x/crypto/nacl/sign" - io "io" + //@ ev "github.com/ModularVerification/ReusableVerificationLibrary/event" //@ "github.com/ModularVerification/ReusableVerificationLibrary/label" //@ "github.com/ModularVerification/ReusableVerificationLibrary/labeling" @@ -20,7 +22,6 @@ import ( //@ u "github.com/ModularVerification/ReusableVerificationLibrary/usage" ) - type ByteString []byte // wraps IO calls and crypto @@ -33,7 +34,6 @@ const GroupGenerator = 2 const GroupSizeString = "FFFFFFFFFFFFFFFFC90FDAA22168C234C4C6628B80DC1CD129024E088A67CC74020BBEA63B139B22514A08798E3404DDEF9519B3CD3A431B302B0A6DF25F14374FE1356D6D51C245E485B576625E7EC6F44C42E9A637ED6B0BFF5CB6F406B7EDEE386BFB5A899FA5AE9F24117C4B1FE649286651ECE45B3DC2007CB8A163BF0598DA48361C55D39A69163FA8FD24CF5F83655D23DCA3AD961C62F356208552BB9ED529077096966D670C354E4ABC9804F1746C08CA18217C32905E462E36CE3BE39E772C180E86039B2783A2EC07A28FB5C55DF06F4C52C9DE2BCBF6955817183995497CEA956AE515D2261898FA051015728E5A8AACAA68FFFFFFFFFFFFFFFF" const DHHalfKeyLength = 256 - type LibraryState struct { // we need at least a field to not run into unknown equality issues dummy int @@ -59,16 +59,19 @@ pred Mem(s ByteString) // { // } ghost +decreases requires acc(Mem(b), _) ensures Size(b) == 0 ==> res == tm.zeroStringB(0) pure func Abs(b ByteString) (res tm.Bytes) ghost +decreases ensures Mem(res) && Abs(res) == bytes // allocates a new slice of bytes and sets the elements according to `bytes` func NewByteStringWithContent(bytes tm.Bytes) (res ByteString) ghost +decreases requires b != nil ==> acc(Mem(b), _) ensures b != nil ? res == Abs(b) : res == tm.zeroStringB(l) pure func SafeAbs(b ByteString, l int) (res tm.Bytes) @@ -77,6 +80,7 @@ pure func SafeAbs(b ByteString, l int) (res tm.Bytes) pred IsNonce(b tm.Bytes) @*/ +//@ decreases //@ requires acc(Mem(b), _) //@ ensures res >= 0 && res == len(b) //@ pure @@ -90,7 +94,30 @@ func Size(b ByteString) (res int) { //@ ensures err == nil ==> Abs(pk) == tm.createPkB(Abs(sk)) && Abs(sk) == tm.gamma(tm.random(Abs(sk), keyLabel, u.PkeKey(usageString))) //@ ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(sk), keyLabel, u.PkeKey(usageString))) //@ ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(sk), keyLabel, u.PkeKey(usageString)), eventType) -func (l *LibraryState) GeneratePkeKey(/*@ ghost ctx labeling.LabelingContext, ghost keyLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/) (pk, sk ByteString, err error) { +func (l *LibraryState) GeneratePkeKey( /*@ ghost ctx labeling.LabelingContext, ghost keyLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/ ) (pk, sk ByteString, err error) { + privateKey, err := rsa.GenerateKey(rand.Reader, 4096) + if err != nil { + return + } + publicKey := privateKey.Public() + + // we serialize the private and public key as PKCS #1, ASN.1 DER and PKIX, ASN.1 DER, respectively. + sk = x509.MarshalPKCS1PrivateKey(privateKey) + + pk, err = x509.MarshalPKIXPublicKey(publicKey) + return +} + +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +ensures err == nil ==> Mem(pk) && Mem(sk) +ensures err == nil ==> Abs(pk) == tm.createPkB(Abs(sk)) && Abs(sk) == tm.gamma(tm.random(Abs(sk), keyLabel, u.PkeKey(usageString))) +ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(sk), keyLabel, u.PkeKey(usageString))) +ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(sk), keyLabel, u.PkeKey(usageString)), eventType) +func (l *LibraryState) AttackerGeneratePkeKey(ctx labeling.LabelingContext, keyLabel label.SecrecyLabel, usageString string, eventTypes set[ev.EventType]) (pk, sk ByteString, err error) { privateKey, err := rsa.GenerateKey(rand.Reader, 4096) if err != nil { return @@ -103,6 +130,7 @@ func (l *LibraryState) GeneratePkeKey(/*@ ghost ctx labeling.LabelingContext, gh pk, err = x509.MarshalPKIXPublicKey(publicKey) return } +@*/ //@ trusted //@ preserves acc(l.Mem(), 1/16) @@ -110,7 +138,29 @@ func (l *LibraryState) GeneratePkeKey(/*@ ghost ctx labeling.LabelingContext, gh //@ ensures err == nil ==> Abs(key) == tm.gamma(tm.random(Abs(key), keyLabel, u.DhKey(usageString))) //@ ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(key), keyLabel, u.DhKey(usageString))) //@ ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(key), keyLabel, u.DhKey(usageString)), eventType) -func (l *LibraryState) GenerateDHKey(/*@ ghost ctx labeling.LabelingContext, ghost keyLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/) (key ByteString, err error) { +func (l *LibraryState) GenerateDHKey( /*@ ghost ctx labeling.LabelingContext, ghost keyLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/ ) (key ByteString, err error) { + var keyBuf [32]byte + key = keyBuf[:] + _, err = rand.Read(key) + if err != nil { + return + } + // clamp + key[0] &= 248 + key[31] = (key[31] & 127) | 64 + return +} + +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +ensures err == nil ==> Mem(key) && Size(key) == 32 +ensures err == nil ==> Abs(key) == tm.gamma(tm.random(Abs(key), keyLabel, u.DhKey(usageString))) +ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(key), keyLabel, u.DhKey(usageString))) +ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(key), keyLabel, u.DhKey(usageString)), eventType) +func (l *LibraryState) AttackerGenerateDHKey(ctx labeling.LabelingContext, keyLabel label.SecrecyLabel, usageString string, eventTypes set[ev.EventType]) (key ByteString, err error) { var keyBuf [32]byte key = keyBuf[:] _, err = rand.Read(key) @@ -122,6 +172,7 @@ func (l *LibraryState) GenerateDHKey(/*@ ghost ctx labeling.LabelingContext, gho key[31] = (key[31] & 127) | 64 return } +@*/ //@ trusted //@ preserves acc(l.Mem(), 1/16) @@ -129,7 +180,7 @@ func (l *LibraryState) GenerateDHKey(/*@ ghost ctx labeling.LabelingContext, gho //@ ensures err == nil ==> Abs(pk) == tm.createPkB(Abs(sk)) && Abs(sk) == tm.gamma(tm.random(Abs(sk), keyLabel, u.SigningKey(usageString))) //@ ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(sk), keyLabel, u.SigningKey(usageString))) //@ ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(sk), keyLabel, u.SigningKey(usageString)), eventType) -func (l *LibraryState) GenerateSigningKey(/*@ ghost ctx labeling.LabelingContext, ghost keyLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/) (pk, sk ByteString, err error) { +func (l *LibraryState) GenerateSigningKey( /*@ ghost ctx labeling.LabelingContext, ghost keyLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/ ) (pk, sk ByteString, err error) { publicKey, privateKey, err := sign.GenerateKey(rand.Reader) if err != nil { return @@ -146,13 +197,31 @@ func (l *LibraryState) GenerateSigningKey(/*@ ghost ctx labeling.LabelingContext //@ ensures err == nil ==> Abs(nonce) == tm.gamma(tm.random(Abs(nonce), nonceLabel, u.Nonce(usageString))) //@ ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(nonce), nonceLabel, u.Nonce(usageString))) //@ ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(nonce), nonceLabel, u.Nonce(usageString)), eventType) -func (l *LibraryState) CreateNonce(/*@ ghost ctx labeling.LabelingContext, ghost nonceLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/) (nonce ByteString, err error) { +func (l *LibraryState) CreateNonce( /*@ ghost ctx labeling.LabelingContext, ghost nonceLabel label.SecrecyLabel, ghost usageString string, ghost eventTypes set[ev.EventType] @*/ ) (nonce ByteString, err error) { + var nonceArr [NonceLength]byte + nonce = nonceArr[:] + io.ReadFull(rand.Reader, nonce) + // inhale `NonceIsUnique` and `NonceForEventIsUnique` instances + return nonce, nil +} + +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +ensures err == nil ==> Mem(nonce) && Size(nonce) == NonceLength +ensures err == nil ==> Abs(nonce) == tm.gamma(tm.random(Abs(nonce), nonceLabel, u.Nonce(usageString))) +ensures err == nil ==> ctx.NonceIsUnique(tm.random(Abs(nonce), nonceLabel, u.Nonce(usageString))) +ensures err == nil ==> forall eventType ev.EventType :: { eventType in eventTypes } eventType in eventTypes ==> ctx.NonceForEventIsUnique(tm.random(Abs(nonce), nonceLabel, u.Nonce(usageString)), eventType) +func (l *LibraryState) GhostCreateNonce(ctx labeling.LabelingContext, nonceLabel label.SecrecyLabel, usageString string, eventTypes set[ev.EventType]) (nonce ByteString, err error) { var nonceArr [NonceLength]byte nonce = nonceArr[:] io.ReadFull(rand.Reader, nonce) // inhale `NonceIsUnique` and `NonceForEventIsUnique` instances return nonce, nil } +@*/ //@ trusted //@ preserves acc(l.Mem(), 1/16) @@ -169,18 +238,50 @@ func (l *LibraryState) Enc(msg, pk ByteString) (ciphertext ByteString, err error var rsaPublicKey *rsa.PublicKey switch publicKey := publicKey.(type) { - case *rsa.PublicKey: - rsaPublicKey = publicKey - break - default: - err = errors.New("invalid public key") - return - } + case *rsa.PublicKey: + rsaPublicKey = publicKey + break + default: + err = errors.New("invalid public key") + return + } + + rng := rand.Reader + ciphertext, err = rsa.EncryptOAEP(sha256.New(), rng, rsaPublicKey, msg, nil) + return +} + +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +preserves acc(Mem(msg), 1/16) +preserves acc(Mem(pk), 1/16) +ensures err == nil ==> Mem(ciphertext) +ensures err == nil ==> Abs(ciphertext) == tm.encryptB(Abs(msg), Abs(pk)) +func (l *LibraryState) AttackerEnc(msg, pk ByteString) (ciphertext ByteString, err error) { + // unmarshal pk: + publicKey, err := x509.ParsePKIXPublicKey(pk) + if err != nil { + return + } + + var rsaPublicKey *rsa.PublicKey + switch publicKey := publicKey.(type) { + case *rsa.PublicKey: + rsaPublicKey = publicKey + break + default: + err = errors.New("invalid public key") + return + } rng := rand.Reader ciphertext, err = rsa.EncryptOAEP(sha256.New(), rng, rsaPublicKey, msg, nil) return } +@*/ //@ trusted //@ preserves acc(l.Mem(), 1/16) @@ -200,6 +301,28 @@ func (l *LibraryState) Dec(ciphertext, sk ByteString) (msg ByteString, err error return } +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +preserves acc(Mem(ciphertext), 1/16) +preserves acc(Mem(sk), 1/16) +ensures err == nil ==> Mem(msg) +ensures err == nil ==> Abs(ciphertext) == tm.encryptB(Abs(msg), tm.createPkB(Abs(sk))) +func (l *LibraryState) AttackerDec(ciphertext, sk ByteString) (msg ByteString, err error) { + // unmarshal sk: + privateKey, err := x509.ParsePKCS1PrivateKey(sk) + if err != nil { + return + } + + rng := rand.Reader + msg, err = rsa.DecryptOAEP(sha256.New(), rng, privateKey, ciphertext, nil) + return +} +@*/ + //@ trusted //@ preserves acc(l.Mem(), 1/16) //@ requires acc(Mem(key), 1/16) && acc(Mem(nonce), 1/16) @@ -219,6 +342,29 @@ func (l *LibraryState) AeadEnc(key, nonce, plaintext, additionalData ByteString) return } +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +requires acc(Mem(key), 1/16) && acc(Mem(nonce), 1/16) +requires Size(key) == 32 && Size(nonce) == 12 +preserves plaintext != nil ==> acc(Mem(plaintext), 1/16) +preserves additionalData != nil ==> acc(Mem(additionalData), 1/16) +ensures acc(Mem(key), 1/16) && acc(Mem(nonce), 1/16) +ensures err == nil ==> Mem(ciphertext) && Size(ciphertext) == (plaintext == nil ? 0 : Size(plaintext)) + 16 +ensures err == nil ==> Abs(ciphertext) == tm.aeadB(Abs(key), Abs(nonce), SafeAbs(plaintext, 0), SafeAbs(additionalData, 0)) +func (l *LibraryState) AttackerAeadEnc(key, nonce, plaintext, additionalData ByteString) (ciphertext ByteString, err error) { + aead, err := chacha20poly1305.New(key) + if err != nil { + return + } + ciphertext = make([]byte, len(plaintext)+16) + aead.Seal(ciphertext[:0], nonce, plaintext, additionalData) + return +} +@*/ + //@ trusted //@ preserves acc(l.Mem(), 1/16) //@ requires acc(Mem(key), 1/16) && acc(Mem(nonce), 1/16) @@ -238,6 +384,29 @@ func (l *LibraryState) AeadDec(key, nonce, ciphertext, additionalData ByteString return } +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +requires acc(Mem(key), 1/16) && acc(Mem(nonce), 1/16) +requires Size(key) == 32 && Size(nonce) == 12 +preserves acc(Mem(ciphertext), 1/16) +preserves additionalData != nil ==> acc(Mem(additionalData), 1/16) +ensures acc(Mem(key), 1/16) && acc(Mem(nonce), 1/16) +ensures err == nil ==> Mem(res) && Size(res) == Size(ciphertext) - 16 +ensures err == nil ==> Abs(ciphertext) == tm.aeadB(Abs(key), Abs(nonce), Abs(res), SafeAbs(additionalData, 0)) +func (l *LibraryState) AttackerAeadDec(key, nonce, ciphertext, additionalData ByteString) (res ByteString, err error) { + aead, err := chacha20poly1305.New(key) + if err != nil { + return + } + res = make([]byte, len(ciphertext)-16) + _, err = aead.Open(res[:0], nonce, ciphertext, additionalData) + return +} +@*/ + //@ trusted //@ preserves acc(l.Mem(), 1/16) //@ preserves acc(Mem(data), 1/16) && acc(Mem(sk), 1/16) @@ -255,6 +424,27 @@ func (l *LibraryState) Sign(data []byte, sk []byte) (res []byte, err error) { return sign.Sign(out, data, &skBuf), nil } +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +preserves acc(Mem(data), 1/16) && acc(Mem(sk), 1/16) +ensures err == nil ==> Mem(res) +ensures err == nil ==> Abs(res) == tm.signB(Abs(data), Abs(sk)) +func (l *LibraryState) AttackerSign(data []byte, sk []byte) (res []byte, err error) { + if len(sk) != 64 { + return nil, errors.New("invalid secret key") + } + var skBuf [64]byte + copy(skBuf[:], sk) + + var out []byte + // not that the (64 bytes) signature is prepended to the plaintext + return sign.Sign(out, data, &skBuf), nil +} +@*/ + //@ trusted //@ preserves acc(l.Mem(), 1/16) //@ preserves acc(Mem(signedData), 1/16) @@ -269,7 +459,34 @@ func (l *LibraryState) Open(signedData []byte, pk []byte /*@, ghost skT tm.Term } var pkBuf [32]byte copy(pkBuf[:], pk) - + + var out []byte + data, success := sign.Open(out, signedData, &pkBuf) + if success { + return data, nil + } else { + return nil, errors.New("signature check has failed") + } +} + +/*@ +ghost +trusted +decreases +preserves acc(l.Mem(), 1/16) +preserves acc(Mem(signedData), 1/16) +requires acc(Mem(pk), 1/16) +requires Abs(pk) == tm.gamma(tm.createPk(skT)) +ensures acc(Mem(pk), 1/16) +ensures err == nil ==> Mem(res) +ensures err == nil ==> Abs(signedData) == tm.signB(Abs(res), tm.gamma(skT)) +func (l *LibraryState) AttackerOpen(signedData []byte, pk []byte, skT tm.Term) (res []byte, err error) { + if len(pk) != 32 { + return nil, errors.New("invalid public key") + } + var pkBuf [32]byte + copy(pkBuf[:], pk) + var out []byte data, success := sign.Open(out, signedData, &pkBuf) if success { @@ -278,6 +495,7 @@ func (l *LibraryState) Open(signedData []byte, pk []byte /*@, ghost skT tm.Term return nil, errors.New("signature check has failed") } } +@*/ //@ trusted //@ preserves acc(l.Mem(), 1/16) diff --git a/labeledlibrary/library/utils.go b/labeledlibrary/library/utils.go index 28c42ae..44e1bee 100644 --- a/labeledlibrary/library/utils.go +++ b/labeledlibrary/library/utils.go @@ -6,7 +6,6 @@ import ( fmt "fmt" ) - //@ trusted //@ decreases //@ requires acc(Mem(s1), 1/16) @@ -24,8 +23,18 @@ func Compare(s1, s2 ByteString) (res bool) { //@ decreases //@ ensures res != nil func NewError(desc string) (res error) { - return errors.New("idB does not match") + return errors.New(desc) +} + +/*@ +ghost +trusted +decreases +ensures res != nil +func AttackerNewError(desc string) (res error) { + return errors.New(desc) } +@*/ //@ trusted //@ decreases diff --git a/labeledlibrary/security-properties.gobra b/labeledlibrary/security-properties.gobra index cd13724..475b6ff 100644 --- a/labeledlibrary/security-properties.gobra +++ b/labeledlibrary/security-properties.gobra @@ -14,6 +14,7 @@ import ( // #region Security Properties ghost +decreases requires acc(l.Mem(), _) // A term is secret if it is either unknown to the attacker or one of its readers (i.e. `honestIds`) // has been corrupted. Currently, this property is restricted to the `Readers` label @@ -25,6 +26,7 @@ pure func (l *LabeledLibrary) Secrecy(term tm.Term, honestIds set[p.Id]) bool { } ghost +decreases requires prev.isSuffix(snapshot) // `honestIds` can be corrupted at any time and `prevHonestIds` must have been already been corrupted at `prev` // in order that `term` is considered forward secret despite the attacker knowing the value. @@ -35,6 +37,7 @@ pure func ForwardSecrecy(snapshot, prev tr.TraceEntry, term tm.Term, prevHonestI } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) NonInjectiveAgreement(actor, peer p.Principal, commit, running ev.Event, honestIds set[p.Id]) bool { return l.Ctx().EventConsistency(running) && @@ -47,6 +50,7 @@ pure func (l *LabeledLibrary) NonInjectiveAgreement(actor, peer p.Principal, com } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) InjectiveAgreement(actor, peer p.Principal, commit, running ev.Event, honestIds set[p.Id]) bool { return l.NonInjectiveAgreement(actor, peer, commit, running, honestIds) && @@ -57,6 +61,7 @@ pure func (l *LabeledLibrary) InjectiveAgreement(actor, peer p.Principal, commit } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) EventIsUnique(principal p.Principal, event ev.Event) bool { return l.Ctx().EventConsistency(event) && diff --git a/labeledlibrary/state.go b/labeledlibrary/state.go index 3723cd9..c6bf6a9 100644 --- a/labeledlibrary/state.go +++ b/labeledlibrary/state.go @@ -16,13 +16,12 @@ import ( //@ u "github.com/ModularVerification/ReusableVerificationLibrary/usage" ) -// TODO ghost fields should be ghost type LabeledLibrary struct { - s *lib.LibraryState + s *lib.LibraryState com Communication - //@ ctx tri.TraceContext - //@ manager *tman.TraceManager - //@ owner p.Id + //@ ghost ctx tri.TraceContext + //@ ghost manager gpointer[tman.TraceManager] + //@ ghost owner p.Id } /*@ @@ -36,19 +35,20 @@ pred (l *LabeledLibrary) Mem() { } // abstract over all memory that remains unchanged after library initialization -// TODO should be ghost -type ImmutableState struct { +ghost type ImmutableState ghost struct { l LabeledLibrary // the entire struct remains constant after initialization managerState tman.ImmutableState } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) ImmutableState() ImmutableState { return unfolding acc(l.Mem(), _) in ImmutableState{ *l, l.manager.ImmutableState(l.ctx, l.owner) } } ghost +decreases requires acc(l.Mem(), _) ensures res != nil && isComparable(res) && res.Props() pure func (l *LabeledLibrary) Ctx() (res tri.TraceContext) { @@ -56,30 +56,35 @@ pure func (l *LabeledLibrary) Ctx() (res tri.TraceContext) { } ghost +decreases requires acc(l.Mem(), _) -pure func (l *LabeledLibrary) Manager() *tman.TraceManager { +pure func (l *LabeledLibrary) Manager() gpointer[tman.TraceManager] { return unfolding acc(l.Mem(), _) in l.manager } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) Owner() p.Id { return unfolding acc(l.Mem(), _) in l.owner } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) OwnerWoThread() p.Id { return unfolding acc(l.Mem(), _) in l.owner.IsSessionThread() ? p.sessionId(p.getIdPrincipal(l.owner), p.getIdSession(l.owner)) : l.owner } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) LabelCtx() labeling.LabelingContext { return tri.GetLabeling(l.Ctx()) } ghost +decreases requires acc(l.Mem(), _) pure func (l *LabeledLibrary) Snapshot() tr.TraceEntry { return unfolding acc(l.Mem(), _) in l.manager.Snapshot(l.ctx, l.owner) @@ -97,9 +102,15 @@ pure func (l *LabeledLibrary) Snapshot() tr.TraceEntry { //@ ensures res.Owner() == owner //@ ensures (res.ImmutableState()).managerState == old(manager.ImmutableState(ctx, owner)) //@ ensures res.Snapshot() == old(manager.Snapshot(ctx, owner)) -// TODO manager, ctx, owner should be ghost -func NewLabeledLibrary(s *lib.LibraryState, com Communication /*@, manager *tman.TraceManager, ctx tri.TraceContext, owner p.Id @*/) (res *LabeledLibrary) { - res = &LabeledLibrary{ s, com /*@, ctx, manager, owner @*/ } +func NewLabeledLibrary(s *lib.LibraryState, com Communication /*@, ghost manager gpointer[tman.TraceManager], ghost ctx tri.TraceContext, ghost owner p.Id @*/) (res *LabeledLibrary) { + // the following line is currently not accepted by Gobra's type-checker (see https://github.com/viperproject/gobra/issues/876): + // res = &LabeledLibrary{s, com /*@, ctx, manager, owner @*/} + res = new(LabeledLibrary) + res.s = s + res.com = com + //@ res.ctx = ctx + //@ res.manager = manager + //@ res.owner = owner //@ fold res.Mem() return } @@ -439,7 +450,9 @@ func (l *LabeledLibrary) PublishedTermImpliesMadePublicInvWithSnap(snap tr.Trace } ghost +decreases requires l.Mem() +requires isComparable(event.params) requires (l.Ctx()).eventInv(l.Owner().getPrincipal(), event, l.Snapshot()) ensures l.Mem() ensures l.ImmutableState() == old(l.ImmutableState()) diff --git a/labeling/key-type.gobra b/labeling/key-type.gobra index b4d9156..d5d1c9b 100644 --- a/labeling/key-type.gobra +++ b/labeling/key-type.gobra @@ -1,6 +1,6 @@ package labeling -type KeyType domain { +ghost type KeyType domain { // constructors // type 0 func KeyTypePke() KeyType @@ -43,5 +43,6 @@ type KeyType domain { } } +ghost decreases func GetArbKeyType() KeyType diff --git a/labeling/label-preservation.gobra b/labeling/label-preservation.gobra index 342d173..c5edfd7 100644 --- a/labeling/label-preservation.gobra +++ b/labeling/label-preservation.gobra @@ -10,6 +10,7 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" // inputs ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -19,6 +20,7 @@ func (ctx LabelingContext) tuple2(t tr.TraceEntry, t1, t2 tm.Term, l label.Secre } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -29,6 +31,7 @@ func (ctx LabelingContext) tuple3(t tr.TraceEntry, t1, t2, t3 tm.Term, l label.S } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -40,6 +43,7 @@ func (ctx LabelingContext) tuple4(t tr.TraceEntry, t1, t2, t3, t4 tm.Term, l lab } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -52,6 +56,7 @@ func (ctx LabelingContext) tuple5(t tr.TraceEntry, t1, t2, t3, t4, t5 tm.Term, l } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -66,6 +71,7 @@ func (ctx LabelingContext) tuple7(t tr.TraceEntry, t1, t2, t3, t4, t5, t6, t7 tm } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, input, l) ensures ctx.IsMsg(t, tm.hash(input), l) @@ -74,6 +80,7 @@ func (ctx LabelingContext) hash(t tr.TraceEntry, input tm.Term, l label.SecrecyL } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, input, l) ensures ctx.IsMsg(t, tm.kdf1(input), l) @@ -84,6 +91,7 @@ func (ctx LabelingContext) kdf(t tr.TraceEntry, input tm.Term, l label.SecrecyLa } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, input, l) ensures ctx.IsMsg(t, tm.createPk(input), l) @@ -92,6 +100,7 @@ func (ctx LabelingContext) createPk(t tr.TraceEntry, input tm.Term, l label.Secr } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, pk, l) requires ctx.IsMsg(t, plaintext, l) @@ -103,6 +112,7 @@ func (ctx LabelingContext) encrypt(t tr.TraceEntry, pk, plaintext tm.Term, l lab } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, key, l) requires ctx.IsMsg(t, nonce, l) @@ -116,6 +126,7 @@ func (ctx LabelingContext) aead(t tr.TraceEntry, key, nonce, plaintext, auth tm. } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.const1(), l) func (ctx LabelingContext) const1(t tr.TraceEntry, l label.SecrecyLabel) { @@ -123,6 +134,7 @@ func (ctx LabelingContext) const1(t tr.TraceEntry, l label.SecrecyLabel) { } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -158,6 +170,7 @@ func (ctx LabelingContext) exp(t tr.TraceEntry, t1, t2 tm.Term, l label.SecrecyL } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, t1, l) requires ctx.IsMsg(t, t2, l) @@ -167,6 +180,7 @@ func (ctx LabelingContext) mult(t tr.TraceEntry, t1, t2 tm.Term, l label.Secrecy } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.stringTerm(s), l) func (ctx LabelingContext) stringTerm(t tr.TraceEntry, s string, l label.SecrecyLabel) { @@ -174,6 +188,7 @@ func (ctx LabelingContext) stringTerm(t tr.TraceEntry, s string, l label.Secrecy } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.zeroString(n), l) func (ctx LabelingContext) zeroString(t tr.TraceEntry, n int, l label.SecrecyLabel) { @@ -181,6 +196,7 @@ func (ctx LabelingContext) zeroString(t tr.TraceEntry, n int, l label.SecrecyLab } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.integer64(n), l) func (ctx LabelingContext) integer64(t tr.TraceEntry, n uint64, l label.SecrecyLabel) { @@ -188,6 +204,7 @@ func (ctx LabelingContext) integer64(t tr.TraceEntry, n uint64, l label.SecrecyL } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.integer32(n), l) func (ctx LabelingContext) integer32(t tr.TraceEntry, n uint32, l label.SecrecyLabel) { @@ -195,6 +212,7 @@ func (ctx LabelingContext) integer32(t tr.TraceEntry, n uint32, l label.SecrecyL } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.infoTerm(), l) func (ctx LabelingContext) infoTerm(t tr.TraceEntry, l label.SecrecyLabel) { @@ -202,6 +220,7 @@ func (ctx LabelingContext) infoTerm(t tr.TraceEntry, l label.SecrecyLabel) { } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.prologueTerm(), l) func (ctx LabelingContext) prologueTerm(t tr.TraceEntry, l label.SecrecyLabel) { @@ -209,6 +228,7 @@ func (ctx LabelingContext) prologueTerm(t tr.TraceEntry, l label.SecrecyLabel) { } ghost +decreases requires ctx.Props() ensures ctx.IsMsg(t, tm.generator(), l) func (ctx LabelingContext) generator(t tr.TraceEntry, l label.SecrecyLabel) { @@ -221,6 +241,7 @@ func (ctx LabelingContext) generator(t tr.TraceEntry, l label.SecrecyLabel) { // an implementation. For example, we do not show label preservation for deconstructing // a hash since such a method does not exist in practice. ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.tuple2(t1, t2), l) ensures ctx.IsMsg(t, t1, l) @@ -230,6 +251,7 @@ func (ctx LabelingContext) untuple2(t tr.TraceEntry, t1, t2 tm.Term, l label.Sec } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.tuple3(t1, t2, t3), l) ensures ctx.IsMsg(t, t1, l) @@ -240,6 +262,7 @@ func (ctx LabelingContext) untuple3(t tr.TraceEntry, t1, t2, t3 tm.Term, l label } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.tuple4(t1, t2, t3, t4), l) ensures ctx.IsMsg(t, t1, l) @@ -251,6 +274,7 @@ func (ctx LabelingContext) untuple4(t tr.TraceEntry, t1, t2, t3, t4 tm.Term, l l } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.tuple5(t1, t2, t3, t4, t5), l) ensures ctx.IsMsg(t, t1, l) @@ -263,6 +287,7 @@ func (ctx LabelingContext) untuple5(t tr.TraceEntry, t1, t2, t3, t4, t5 tm.Term, } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.tuple7(t1, t2, t3, t4, t5, t6, t7), l) ensures ctx.IsMsg(t, t1, l) @@ -277,6 +302,7 @@ func (ctx LabelingContext) untuple7(t tr.TraceEntry, t1, t2, t3, t4, t5, t6, t7 } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.encrypt(plaintext, tm.createPk(sk)), l) requires ctx.IsMsg(t, sk, l) // knowing the secret key is a requirement for decryption @@ -291,6 +317,7 @@ func (ctx LabelingContext) decrypt(t tr.TraceEntry, plaintext, sk tm.Term, l lab } ghost +decreases requires ctx.Props() requires ctx.IsMsg(t, tm.aead(key, nonce, plaintext, ad), l) requires ctx.IsMsg(t, key, l) // knowing the key is a requirement for decryption diff --git a/labeling/labeling.gobra b/labeling/labeling.gobra index 5a29b78..efdd672 100644 --- a/labeling/labeling.gobra +++ b/labeling/labeling.gobra @@ -11,7 +11,7 @@ import . "github.com/ModularVerification/ReusableVerificationLibrary/usagecontex /** alias */ -type IdSet = set[p.Id] +ghost type IdSet = set[p.Id] /** * overview over some lemmas available in this file on the level of `canFlowInternal_DYStar @@ -1096,6 +1096,7 @@ pure func (ctx LabelingContext) canFlowInternal(corruptIds set[p.Id], l1, l2 lab } ghost +decreases label.GetHeight(l1), label.GetHeight(l2) /** * this is the orginal `can_flow` function used by DY*. * we show below that `canFlowInternal` and `canFlowInternal_DYStar` are equivalent. @@ -1966,9 +1967,11 @@ pred (ctx LabelingContext) NonceForEventIsUnique(nonce tm.Term, eventType ev.Eve // results in a contradiction when unfolding the predicate instances type Void int // note that `struct{}` results in Gobra not generating the expected heap permissions ghost +decreases pure func (ctx LabelingContext) getNonceIsUniquePointer(nonce tm.Term) *Void ghost +decreases pure func (ctx LabelingContext) getNonceForEventIsUniquePointer(nonce tm.Term, eventType ev.EventType) *Void ghost diff --git a/local-verify.sh b/local-verify.sh index 92fe463..cc926d4 100755 --- a/local-verify.sh +++ b/local-verify.sh @@ -8,8 +8,8 @@ scriptDir=$(dirname "$0") isCi=$CI # gobraJar="/gobra/gobra.jar" -gobraJar="/Users/LinardArquint/gobra/target/scala-2.13/gobra.jar" -additionalGobraArgs="--module github.com/ModularVerification/ReusableVerificationLibrary --include .verification --z3Exe /Users/LinardArquint/.local/bin/z3 --parallelizeBranches" +gobraJar="/Users/arquintlinard/ETH/PhD/gobra/target/scala-2.13/gobra.jar" +additionalGobraArgs="--module github.com/ModularVerification/ReusableVerificationLibrary --include .verification --z3Exe /Users/arquintlinard/.local/bin/z3 --parallelizeBranches" if [ $isCi ]; then echo -e "\033[0Ksection_start:`date +%s`:verify[collapsed=true]\r\033[0KVerifying packages" diff --git a/principal/principal.go b/principal/principal.go index 0dd1fc6..dfed5ff 100644 --- a/principal/principal.go +++ b/principal/principal.go @@ -3,13 +3,13 @@ package principal type Principal = string /*@ -type Id domain { +ghost type Id domain { // constructors // type 0 func principalId(Principal) Id // type 1 func sessionId(Principal, uint32) Id - // type 2; similar to type1 but allows to distinguish between + // type 2; similar to type1 but allows to distinguish between // different threads belonging to the same session func sessionThreadId(Principal, uint32, uint32) Id // type 3 @@ -70,7 +70,7 @@ type Id domain { } } -// TODO this should be ghost +ghost decreases ensures res == principalId(principal) pure func NewPrincipalId(principal Principal) (res Id) diff --git a/term/bytes.gobra b/term/bytes.gobra index 4f5174a..0ba8100 100644 --- a/term/bytes.gobra +++ b/term/bytes.gobra @@ -1,6 +1,6 @@ package term -type Bytes domain { +ghost type Bytes domain { // constructors func tuple2B(Bytes, Bytes) Bytes @@ -96,7 +96,7 @@ type Bytes domain { } } -type Gamma domain { +ghost type Gamma domain { func gamma(Term) Bytes func oneTerm(Bytes) Term diff --git a/term/term.gobra b/term/term.gobra index 41a1dff..65d6a64 100644 --- a/term/term.gobra +++ b/term/term.gobra @@ -12,7 +12,7 @@ import u "github.com/ModularVerification/ReusableVerificationLibrary/usage" * all have the same height. */ -type Term domain { +ghost type Term domain { // type 0 func random(Bytes, label.SecrecyLabel, u.Usage) Term func getRandomBytes(Term) Bytes @@ -574,12 +574,16 @@ pure func decrypt(ciphertext, sk Term) option[Term] { none[Term] // not a ciphertext } +ghost +decreases requires decrypt(ciphertext, sk) == some(plaintext) ensures ciphertext == encrypt(plaintext, createPk(sk)) func pkeDecLemma(sk Term, ciphertext Term, plaintext Term) { // no body needed } +ghost +decreases requires sk1 != sk2 requires ciphertext == encrypt(plaintext, createPk(sk1)) ensures decrypt(ciphertext, sk1) == some(plaintext) diff --git a/trace/entry-helpers.gobra b/trace/entry-helpers.gobra index 05daeb8..dbd7837 100644 --- a/trace/entry-helpers.gobra +++ b/trace/entry-helpers.gobra @@ -54,6 +54,7 @@ decreases pure func (entry TraceEntry) isEventAt(principal p.Principal, ev Event) bool { return entry.isEvent() && getPrincipal(entry) == principal && + isComparable(ev.params) && getEvent(entry) == ev } diff --git a/trace/entry.gobra b/trace/entry.gobra index 5bb1e97..bf58e69 100644 --- a/trace/entry.gobra +++ b/trace/entry.gobra @@ -6,7 +6,7 @@ import p "github.com/ModularVerification/ReusableVerificationLibrary/principal" import tm "github.com/ModularVerification/ReusableVerificationLibrary/term" import u "github.com/ModularVerification/ReusableVerificationLibrary/usage" -type TraceEntry domain { +ghost type TraceEntry domain { // constructors // type 0 func makeRoot(set[tm.Term]) TraceEntry diff --git a/traceinvariant/trace-invariant.gobra b/traceinvariant/trace-invariant.gobra index 804b24b..6e09ed5 100644 --- a/traceinvariant/trace-invariant.gobra +++ b/traceinvariant/trace-invariant.gobra @@ -15,7 +15,7 @@ type TraceContext interface { /** used to express (pure) properties about fields of TraceContext implementations */ pure Props() bool - pred eventInv(principal p.Principal, ev Event, prev TraceEntry) + pred eventInv(principal p.Principal, ghost ev Event, ghost prev TraceEntry) ghost decreases @@ -23,17 +23,17 @@ type TraceContext interface { * Specifies consistency conditions for an event. These conditions * have to be implied by `pureEventInv` */ - pure EventConsistency(ev Event) bool + pure EventConsistency(ghost ev Event) bool ghost decreases - pure pureEventInv(principal p.Principal, ev Event, prev TraceEntry) bool + pure pureEventInv(principal p.Principal, ghost ev Event, ghost prev TraceEntry) bool ghost decreases requires pureEventInv(principal, ev, prev) ensures EventConsistency(ev) - eventInvImpliesConsistency(principal p.Principal, ev Event, prev TraceEntry) + eventInvImpliesConsistency(principal p.Principal, ghost ev Event, ghost prev TraceEntry) ghost decreases @@ -51,7 +51,7 @@ type TraceContext interface { * returns the witness from which event uniqueness can be derived. * This typically is a nonce stored as an event parameter */ - pure UniquenessWitness(ev Event) tm.Term + pure UniquenessWitness(ghost ev Event) (ghost res tm.Term) ghost decreases @@ -62,7 +62,7 @@ type TraceContext interface { ensures nonce == UniquenessWitness(ev) ensures GetLabelingContext(GetUsageContext()).NonceForEventIsUnique(nonce, ev.typ) ensures GetLabelingContext(GetUsageContext()).NonceForEventIsUnique(nonce, ev.typ) --* eventInv(principal, ev, prev) - isUniqueImpliesUniqueResource(principal p.Principal, ev Event, prev TraceEntry) (nonce tm.Term) + isUniqueImpliesUniqueResource(principal p.Principal, ghost ev Event, ghost prev TraceEntry) (ghost nonce tm.Term) ghost decreases @@ -70,21 +70,21 @@ type TraceContext interface { requires acc(eventInv(principal, ev, prev), p) ensures acc(eventInv(principal, ev, prev), p) ensures pureEventInv(principal, ev, prev) - getPureEventInv(principal p.Principal, ev Event, prev TraceEntry, p perm) + getPureEventInv(principal p.Principal, ghost ev Event, ghost prev TraceEntry, ghost p perm) ghost decreases requires t1.isSuffix(t2) requires eventInv(principal, ev, t1) ensures eventInv(principal, ev, t2) - eventInvMonotonic(principal p.Principal, ev Event, t1 TraceEntry, t2 TraceEntry) + eventInvMonotonic(principal p.Principal, ghost ev Event, ghost t1, t2 TraceEntry) ghost decreases requires t1.isSuffix(t2) requires pureEventInv(principal, ev, t1) ensures pureEventInv(principal, ev, t2) - pureEventInvMonotonic(principal p.Principal, ev Event, t1 TraceEntry, t2 TraceEntry) + pureEventInvMonotonic(principal p.Principal, ghost ev Event, ghost t1, t2 TraceEntry) ghost decreases diff --git a/tracemanager/entry-lemmas.gobra b/tracemanager/entry-lemmas.gobra index 9e896b4..82327aa 100644 --- a/tracemanager/entry-lemmas.gobra +++ b/tracemanager/entry-lemmas.gobra @@ -4,7 +4,7 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinvariant" -type EntrySearcher struct { +ghost type EntrySearcher ghost struct { ctx tri.TraceContext entry tr.TraceEntry } diff --git a/tracemanager/event-lemmas.gobra b/tracemanager/event-lemmas.gobra index 125b7f3..9825a59 100644 --- a/tracemanager/event-lemmas.gobra +++ b/tracemanager/event-lemmas.gobra @@ -7,7 +7,7 @@ import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinva /** search for latest matching event (irrespective of a particular trace index) */ -type EventSearcher struct { +ghost type EventSearcher ghost struct { ctx tri.TraceContext principal p.Principal event ev.Event @@ -100,7 +100,7 @@ func (es EventSearcher) ExtractPureEntryInv(entry tr.TraceEntry, p perm) { /** search for matching event taking the trace index into account */ -type EventIdxSearcher struct { +ghost type EventIdxSearcher ghost struct { ctx tri.TraceContext principal p.Principal event ev.Event @@ -207,7 +207,7 @@ ensures prev == snap.eventOccursWitness(principal, event) ensures m.Ctx(ctx, owner).pureEventInv(principal, event, tr.getPrev(prev)) ensures old(m.Snapshot(ctx, owner)) == m.Snapshot(ctx, owner) ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) EventOccursImpliesEventInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, principal p.Principal, event ev.Event) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) EventOccursImpliesEventInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, principal p.Principal, event ev.Event) (prev tr.TraceEntry) { searcher := EventSearcher{ ctx, principal, event } // the following assert stmt is necessary to derive that `ctx != nil`: assert unfolding m.Mem(ctx, owner) in true @@ -231,7 +231,7 @@ ensures idx1 == idx2 ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) ensures m.Snapshot(ctx, owner) == old(m.Snapshot(ctx, owner)) // this lemma is part of the manager as it requires the validTrace predicate -func (m *TraceManager) UniqueEventsAreUniqueAt(ctx tri.TraceContext, owner Client, principal1, principal2 p.Principal, event1, event2 ev.Event, idx1, idx2 int) { +func (m gpointer[TraceManager]) UniqueEventsAreUniqueAt(ctx tri.TraceContext, owner Client, principal1, principal2 p.Principal, event1, event2 ev.Event, idx1, idx2 int) { // to obtain the validTrace predicate instance, we have to aquire the lock and apply monotonicity: inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) @@ -267,7 +267,7 @@ ensures m.Snapshot(ctx, owner).eventOccurs(principal, event) ensures suffix.eventOccursWitness(principal, event) == m.Snapshot(ctx, owner).eventOccursWitness(principal, event) ensures old(m.Snapshot(ctx, owner)) == m.Snapshot(ctx, owner) ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) UniqueEventsOccurOnlyOnce(ctx tri.TraceContext, owner Client, suffix tr.TraceEntry, principal p.Principal, event ev.Event) { +func (m gpointer[TraceManager]) UniqueEventsOccurOnlyOnce(ctx tri.TraceContext, owner Client, suffix tr.TraceEntry, principal p.Principal, event ev.Event) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) suffix.eventOccursMonotonic(lastSeenTrace, principal, event) @@ -318,7 +318,7 @@ ensures s1 == s2 ==> ensures s1 != s2 ==> ctx.eventInv(principal1, event1, tr.getPrev(s1)) && ctx.eventInv(principal2, event2, tr.getPrev(s2)) -func (m *TraceManager) findEvents(ctx tri.TraceContext, validTraceEntry tr.TraceEntry, principal1, principal2 p.Principal, event1, event2 ev.Event, idx1, idx2 int) (s1, s2 tr.TraceEntry) { +func (m gpointer[TraceManager]) findEvents(ctx tri.TraceContext, validTraceEntry tr.TraceEntry, principal1, principal2 p.Principal, event1, event2 ev.Event, idx1, idx2 int) (s1, s2 tr.TraceEntry) { searcher1 := EventIdxSearcher{ ctx, principal1, event1, idx1 } searcher2 := EventIdxSearcher{ ctx, principal2, event2, idx2 } s1, s2 = m.findEntriesWithInv(searcher1, searcher2, validTraceEntry) diff --git a/tracemanager/manager.gobra b/tracemanager/manager.gobra index 61a01af..4f9e219 100644 --- a/tracemanager/manager.gobra +++ b/tracemanager/manager.gobra @@ -11,31 +11,28 @@ import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinva import ts "github.com/ModularVerification/ReusableVerificationLibrary/concurrentdatastructure" -type TraceManager struct { +ghost type TraceManager ghost struct { nClients int - mutex *ts.ClientHistoryMutex + ghost mutex gpointer[ts.ClientHistoryMutex] } -type Client = p.Id +ghost type Client = p.Id // currently necessary because Gobra does apparently not support a dot expression as map key type -type MapKey = p.Id +ghost type MapKey = p.Id +ghost decreases requires ctx != nil && isComparable(ctx) && ctx.Props() requires len(clients) > 0 requires tri.validTrace(ctx, root) requires noPerm < p && p <= writePerm -requires forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> acc(&clients[j], p) requires forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] -ensures forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> acc(&clients[j], p) ensures forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] -ensures acc(ms) +ensures set(clients) == domain(ms) ensures forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> ms[clients[j]].Mem(ctx, clients[j]) ensures forall j, k int :: { clients[j], clients[k] } 0 <= j && j < len(clients) && 0 <= k && k < len(clients) ==> - ms[clients[j]].ImmutableState(ctx, clients[j]) == ms[clients[k]].ImmutableState(ctx, clients[k]) -func NewTraceManager(ctx tri.TraceContext, clients []Client, root tr.TraceEntry, ghost p perm) (ms map[MapKey]*TraceManager) { - ms = make(map[MapKey]*TraceManager) - + ms[clients[j]].ImmutableState(ctx, clients[j]) === ms[clients[k]].ImmutableState(ctx, clients[k]) +func NewTraceManager(ctx tri.TraceContext, clients seq[Client], root tr.TraceEntry, p perm) (ghost ms dict[MapKey]gpointer[TraceManager]) { // forall quantification complains if `inv` is of type ManagerInv instead of ClientHistoryInv: var inv ts.ClientHistoryInv inv = ManagerInv{ ctx } @@ -43,25 +40,17 @@ func NewTraceManager(ctx tri.TraceContext, clients []Client, root tr.TraceEntry, fold inv.CurrentValueInv(root) mutex.SetInv(inv, clients, root, p/2) - // we allocate a slice of trace managers such that we know that the pointers are pairwise distinct: - managers := make([]TraceManager, len(clients)) - invariant 0 <= i && i <= len(clients) - invariant forall j int :: { clients[j] } 0 <= j && j < len(clients) ==> acc(&clients[j], p) invariant forall j, k int :: { clients[j], clients[k] } 0 <= j && j < k && k < len(clients) ==> clients[j] != clients[k] invariant forall j int :: { clients[j] } i <= j && j < len(clients) ==> mutex.ClientHistoryMutexState(inv, clients[j]) - invariant len(clients) == len(managers) - invariant forall j int :: { managers[j] } i <= j && j < len(managers) ==> acc(&managers[j]) - invariant forall j, k int :: { managers[j], managers[k] } 0 <= j && j < k && k < len(managers) ==> &managers[j] != &managers[k] - invariant acc(ms) - invariant forall j int :: { clients[j], managers[j] } 0 <= j && j < i ==> ms[clients[j]] == &managers[j] - invariant forall j int :: { managers[j] } 0 <= j && j < i ==> (&managers[j]).Mem(ctx, clients[j]) + invariant set(clients[:i]) == domain(ms) invariant forall j int :: { clients[j] } 0 <= j && j < i ==> - ((ms[clients[j]].ImmutableState(ctx, clients[j])).mutex == mutex) + ms[clients[j]].Mem(ctx, clients[j]) && + ((ms[clients[j]].ImmutableState(ctx, clients[j])).mutex === mutex) decreases len(clients) - i for i := 0; i < len(clients); i++ { client := clients[i] - m := &managers[i] + m := &TraceManager{} m.nClients = len(clients) m.mutex = mutex ms[client] = m @@ -69,7 +58,7 @@ func NewTraceManager(ctx tri.TraceContext, clients []Client, root tr.TraceEntry, } } -pred (m *TraceManager) Mem(ctx tri.TraceContext, owner Client) { +pred (m gpointer[TraceManager]) Mem(ctx tri.TraceContext, owner Client) { acc(m) && 0 < m.nClients && ctx != nil && isComparable(ctx) && ctx.Props() && m.mutex.ClientHistoryMutexState(ManagerInv{ ctx }, owner) @@ -80,28 +69,27 @@ decreases requires acc(m.Mem(ctx, owner), _) ensures ctx != nil && ctx.Props() // indirection to learn that `ctx != nil` -pure func (m *TraceManager) Ctx(ctx tri.TraceContext, owner Client) tri.TraceContext { +pure func (m gpointer[TraceManager]) Ctx(ctx tri.TraceContext, owner Client) tri.TraceContext { return unfolding acc(m.Mem(ctx, owner), _) in ctx } ghost decreases requires acc(m.Mem(ctx, owner), _) -pure func (m *TraceManager) Snapshot(ctx tri.TraceContext, owner Client) tr.TraceEntry { +pure func (m gpointer[TraceManager]) Snapshot(ctx tri.TraceContext, owner Client) tr.TraceEntry { return unfolding acc(m.Mem(ctx, owner), _) in m.mutex.LastSeenValue(ManagerInv{ ctx }, owner) } // abstract over all memory that remains unchanged after manager initialization -// TODO should be ghost -type ImmutableState struct { - mutex *ts.ClientHistoryMutex +ghost type ImmutableState ghost struct { + mutex gpointer[ts.ClientHistoryMutex] // clients do not need to be included as they follow from pointer equality on the mutex and the `ClientsAreIdentical` lemma } ghost decreases requires acc(m.Mem(ctx, owner), _) -pure func (m *TraceManager) ImmutableState(ctx tri.TraceContext, owner Client) ImmutableState { +pure func (m gpointer[TraceManager]) ImmutableState(ctx tri.TraceContext, owner Client) ImmutableState { return unfolding acc(m.Mem(ctx, owner), _) in ImmutableState{ m.mutex } } @@ -111,10 +99,10 @@ requires m.Mem(ctx, owner) ensures m.Mem(ctx, owner) ensures trace == m.Snapshot(ctx, owner) ensures old(m.Snapshot(ctx, owner)).isSuffix(trace) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) // this method simply updates the local snapshot to the global trace and returns // the updated snapshot for convenience reasons -func (m *TraceManager) Sync(ctx tri.TraceContext, owner Client) (trace tr.TraceEntry) { +func (m gpointer[TraceManager]) Sync(ctx tri.TraceContext, owner Client) (trace tr.TraceEntry) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) @@ -128,12 +116,12 @@ ghost decreases requires destManager.Mem(ctx, destOwner) requires acc(origManager.Mem(ctx, origOwner), 1/8) -requires destManager.ImmutableState(ctx, destOwner) == origManager.ImmutableState(ctx, origOwner) +requires destManager.ImmutableState(ctx, destOwner) === origManager.ImmutableState(ctx, origOwner) ensures destManager.Mem(ctx, destOwner) ensures acc(origManager.Mem(ctx, origOwner), 1/8) ensures (destManager.Snapshot(ctx, destOwner)) == (origManager.Snapshot(ctx, origOwner)) -ensures destManager.ImmutableState(ctx, destOwner) == old(destManager.ImmutableState(ctx, destOwner)) -func (destManager *TraceManager) SetSnapshot(origManager *TraceManager, ctx tri.TraceContext, destOwner, origOwner Client) { +ensures destManager.ImmutableState(ctx, destOwner) === old(destManager.ImmutableState(ctx, destOwner)) +func (destManager gpointer[TraceManager]) SetSnapshot(origManager gpointer[TraceManager], ctx tri.TraceContext, destOwner, origOwner Client) { inv := ManagerInv{ ctx } lastSeenTrace := destManager.Snapshot(ctx, destOwner) unfold destManager.Mem(ctx, destOwner) @@ -153,7 +141,6 @@ func (destManager *TraceManager) SetSnapshot(origManager *TraceManager, ctx tri. fold acc(origManager.mutex.ClientHistoryMutexState(inv, origOwner), 1/8) fold acc(origManager.Mem(ctx, origOwner), 1/8) - *(destManager.mutex.snapshots)[destOwner] = snapshot fold destManager.mutex.ClientHistoryMutexStateLocked(inv, destOwner, trace) destManager.mutex.UnlockWithSnapshot(inv, destOwner, trace, trace, snapshot) fold destManager.Mem(ctx, destOwner) @@ -162,6 +149,7 @@ func (destManager *TraceManager) SetSnapshot(origManager *TraceManager, ctx tri. ghost decreases requires m.Mem(ctx, owner) +requires isComparable(event.params) requires ctx.eventInv(owner.getPrincipal(), event, m.Snapshot(ctx, owner)) ensures m.Mem(ctx, owner) // note that we do not specify here that the event occurs at the most recent trace entry because this property @@ -170,8 +158,8 @@ ensures m.Mem(ctx, owner) // snapshot of the trace. ensures (m.Snapshot(ctx, owner)).isEventAt(owner.getPrincipal(), event) ensures old(m.Snapshot(ctx, owner)).isSuffix(m.Snapshot(ctx, owner)) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) LogEvent(ctx tri.TraceContext, owner Client, event ev.Event) { +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) +func (m gpointer[TraceManager]) LogEvent(ctx tri.TraceContext, owner Client, event ev.Event) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) @@ -193,8 +181,8 @@ requires tri.messageInv(m.Ctx(ctx, owner), sender, receiver, message, m.Snapshot ensures m.Mem(ctx, owner) ensures (m.Snapshot(ctx, owner)).isMessageAt(sender, receiver, message) ensures old(m.Snapshot(ctx, owner)).isSuffix(m.Snapshot(ctx, owner)) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) LogSend(ctx tri.TraceContext, owner Client, sender, receiver p.Principal, message tm.Term) { +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) +func (m gpointer[TraceManager]) LogSend(ctx tri.TraceContext, owner Client, sender, receiver p.Principal, message tm.Term) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) @@ -216,8 +204,8 @@ requires tri.messageInv(m.Ctx(ctx, owner), sender, receiver, message, m.Snapshot ensures m.Mem(ctx, owner) ensures (m.Snapshot(ctx, owner)).isMessageDroppedAt(sender, receiver, message) ensures old(m.Snapshot(ctx, owner)).isSuffix(m.Snapshot(ctx, owner)) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) LogMsgDrop(ctx tri.TraceContext, owner Client, sender, receiver p.Principal, message tm.Term) { +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) +func (m gpointer[TraceManager]) LogMsgDrop(ctx tri.TraceContext, owner Client, sender, receiver p.Principal, message tm.Term) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) @@ -239,8 +227,8 @@ requires tri.madePublicInv(m.Ctx(ctx, owner), term, m.Snapshot(ctx, owner)) ensures m.Mem(ctx, owner) ensures (m.Snapshot(ctx, owner)).isPublic() && tr.getPayload(m.Snapshot(ctx, owner)) == term ensures old(m.Snapshot(ctx, owner)).isSuffix(m.Snapshot(ctx, owner)) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) LogPublish(ctx tri.TraceContext, owner Client, term tm.Term) { +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) +func (m gpointer[TraceManager]) LogPublish(ctx tri.TraceContext, owner Client, term tm.Term) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) @@ -262,8 +250,8 @@ ensures m.Mem(ctx, owner) ensures id in m.Snapshot(ctx, owner).getCorruptIds() ensures tr.containsCorruptId(m.Snapshot(ctx, owner).getCorruptIds(), set[p.Id]{ id }) ensures old(m.Snapshot(ctx, owner)).isSuffix(m.Snapshot(ctx, owner)) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) LogCorruption(ctx tri.TraceContext, owner Client, id p.Id) { +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) +func (m gpointer[TraceManager]) LogCorruption(ctx tri.TraceContext, owner Client, id p.Id) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) @@ -291,8 +279,8 @@ requires tri.GetLabeling(ctx).CanFlow(m.Snapshot(ctx, owner), tm.getRandomLabel( ensures m.Mem(ctx, owner) ensures m.Snapshot(ctx, owner).isNonceAt(nonce) ensures old(m.Snapshot(ctx, owner)).isSuffix(m.Snapshot(ctx, owner)) -ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) LogNonce(ctx tri.TraceContext, owner Client, nonce tm.Term) { +ensures m.ImmutableState(ctx, owner) === old(m.ImmutableState(ctx, owner)) +func (m gpointer[TraceManager]) LogNonce(ctx tri.TraceContext, owner Client, nonce tm.Term) { inv := ManagerInv{ ctx } lastSeenTrace := m.Snapshot(ctx, owner) unfold m.Mem(ctx, owner) diff --git a/tracemanager/message-lemmas.gobra b/tracemanager/message-lemmas.gobra index 280f0cc..4a629bd 100644 --- a/tracemanager/message-lemmas.gobra +++ b/tracemanager/message-lemmas.gobra @@ -6,7 +6,7 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinvariant" -type MessageSearcher struct { +ghost type MessageSearcher ghost struct { ctx tri.TraceContext sender p.Principal receiver p.Principal @@ -108,7 +108,7 @@ ensures prev.isMessageAt(sender, receiver, payload) ensures tri.messageInv(m.Ctx(ctx, owner), sender, receiver, payload, tr.getPrev(prev)) ensures old(m.Snapshot(ctx, owner)) == m.Snapshot(ctx, owner) ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) MessageOccursImpliesMessageInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, sender, receiver p.Principal, payload tm.Term) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) MessageOccursImpliesMessageInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, sender, receiver p.Principal, payload tm.Term) (prev tr.TraceEntry) { searcher := MessageSearcher{ ctx, sender, receiver, payload } // the following assert stmt is necessary to derive that `ctx != nil`: assert unfolding m.Mem(ctx, owner) in true diff --git a/tracemanager/nonce-lemmas.gobra b/tracemanager/nonce-lemmas.gobra index f55c827..5da8622 100644 --- a/tracemanager/nonce-lemmas.gobra +++ b/tracemanager/nonce-lemmas.gobra @@ -5,7 +5,7 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinvariant" -type NonceSearcher struct { +ghost type NonceSearcher ghost struct { ctx tri.TraceContext nonce tm.Term } @@ -105,7 +105,7 @@ ensures prev.isNonceAt(nonce) ensures tri.pureRandInv(ctx, nonce, tr.getPrev(prev)) ensures old(m.Snapshot(ctx, owner)) == m.Snapshot(ctx, owner) ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) NonceOccursImpliesRandInv(ctx tri.TraceContext, owner Client, nonce tm.Term) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) NonceOccursImpliesRandInv(ctx tri.TraceContext, owner Client, nonce tm.Term) (prev tr.TraceEntry) { searcher := NonceSearcher{ ctx, nonce } // the following assert stmt is necessary to derive that `ctx != nil`: assert unfolding m.Mem(ctx, owner) in true diff --git a/tracemanager/public-term-lemmas.gobra b/tracemanager/public-term-lemmas.gobra index 366e21f..f4fdc84 100644 --- a/tracemanager/public-term-lemmas.gobra +++ b/tracemanager/public-term-lemmas.gobra @@ -5,7 +5,7 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinvariant" -type PublicTermSearcher struct { +ghost type PublicTermSearcher ghost struct { ctx tri.TraceContext term tm.Term } @@ -104,7 +104,7 @@ ensures prev.isSuffix(m.Snapshot(ctx, owner)) ensures tri.publicInv(m.Ctx(ctx, owner), snap.getPublicTerms(), prev) ensures old(m.Snapshot(ctx, owner)) == m.Snapshot(ctx, owner) ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) PublicTermImpliesPublicInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, term tm.Term) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) PublicTermImpliesPublicInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, term tm.Term) (prev tr.TraceEntry) { searcher := PublicTermSearcher{ ctx, term } // the following assert stmt is necessary to derive that `ctx != nil`: assert unfolding m.Mem(ctx, owner) in true diff --git a/tracemanager/published-term-lemma.gobra b/tracemanager/published-term-lemma.gobra index 4e7dc8c..013b278 100644 --- a/tracemanager/published-term-lemma.gobra +++ b/tracemanager/published-term-lemma.gobra @@ -5,7 +5,7 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinvariant" -type PublishedTermSearcher struct { +ghost type PublishedTermSearcher ghost struct { ctx tri.TraceContext term tm.Term } @@ -105,7 +105,7 @@ ensures prev.isPublic() ensures tri.madePublicInv(m.Ctx(ctx, owner), term, tr.getPrev(prev)) ensures old(m.Snapshot(ctx, owner)) == m.Snapshot(ctx, owner) ensures m.ImmutableState(ctx, owner) == old(m.ImmutableState(ctx, owner)) -func (m *TraceManager) PublishedTermImpliesMadePublicInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, term tm.Term) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) PublishedTermImpliesMadePublicInvWithSnap(ctx tri.TraceContext, owner Client, snap tr.TraceEntry, term tm.Term) (prev tr.TraceEntry) { searcher := PublishedTermSearcher{ ctx, term } // the following assert stmt is necessary to derive that `ctx != nil`: assert unfolding m.Mem(ctx, owner) in true diff --git a/tracemanager/search.gobra b/tracemanager/search.gobra index 2d554b6..7910a71 100644 --- a/tracemanager/search.gobra +++ b/tracemanager/search.gobra @@ -5,7 +5,7 @@ import tri "github.com/ModularVerification/ReusableVerificationLibrary/traceinva /** represents the state after acquiring the mutex to then use it prove a lemma */ -pred (m *TraceManager) memLocked(ctx tri.TraceContext, owner Client, lastSeenSnapshot, snapshot tr.TraceEntry) { +pred (m gpointer[TraceManager]) memLocked(ctx tri.TraceContext, owner Client, lastSeenSnapshot, snapshot tr.TraceEntry) { acc(m) && 0 < m.nClients && ctx != nil && isComparable(ctx) && ctx.Props() && m.mutex.ClientHistoryMutexStateLocked(ManagerInv{ ctx }, owner, snapshot) && @@ -23,7 +23,7 @@ ensures lastSeenSnapshot.isSuffix(snapshot) ensures m.memLocked(ctx, owner, lastSeenSnapshot, snapshot) ensures old(unfolding m.Mem(ctx, owner) in m.mutex) == unfolding m.memLocked(ctx, owner, lastSeenSnapshot, snapshot) in m.mutex /** utility function to lock mutex and get the valid trace predicate */ -func (m *TraceManager) acquireValidTrace(ctx tri.TraceContext, owner Client) (lastSeenSnapshot, snapshot tr.TraceEntry) { +func (m gpointer[TraceManager]) acquireValidTrace(ctx tri.TraceContext, owner Client) (lastSeenSnapshot, snapshot tr.TraceEntry) { // to obtain the validTrace predicate instance, we have to aquire the lock and apply monotonicity: inv := ManagerInv{ ctx } lastSeenSnapshot := m.Snapshot(ctx, owner) @@ -40,7 +40,7 @@ requires tri.validTrace(ctx, snapshot) ensures m.Mem(ctx, owner) ensures m.Snapshot(ctx, owner) == lastSeenSnapshot ensures (unfolding m.Mem(ctx, owner) in m.mutex) == old(unfolding m.memLocked(ctx, owner, lastSeenSnapshot, snapshot) in m.mutex) -func (m *TraceManager) releaseValidTrace(ctx tri.TraceContext, owner Client, lastSeenSnapshot, snapshot tr.TraceEntry) { +func (m gpointer[TraceManager]) releaseValidTrace(ctx tri.TraceContext, owner Client, lastSeenSnapshot, snapshot tr.TraceEntry) { inv := ManagerInv{ ctx } unfold m.memLocked(ctx, owner, lastSeenSnapshot, snapshot) fold inv.CurrentValueInv(snapshot) @@ -62,7 +62,7 @@ type TraceSearcher interface { ghost decreases - pure Matches(entry tr.TraceEntry) bool + pure Matches(ghost entry tr.TraceEntry) bool ghost decreases @@ -71,22 +71,22 @@ type TraceSearcher interface { /** * states additional (pure) properties about the entry that `Matches` */ - pure MatchProperties(snapshot, entry tr.TraceEntry) bool + pure MatchProperties(ghost snapshot, entry tr.TraceEntry) bool ghost decreases - pure Occurs(entry tr.TraceEntry) bool + pure Occurs(ghost entry tr.TraceEntry) bool ghost decreases requires Props() - pure PureEntryInv(entry tr.TraceEntry) bool + pure PureEntryInv(ghost entry tr.TraceEntry) bool ghost decreases requires Matches(entry) ensures MatchProperties(entry, entry) - MatchPropertiesReflexive(snapshot, entry tr.TraceEntry) + MatchPropertiesReflexive(ghost snapshot, entry tr.TraceEntry) ghost decreases @@ -95,7 +95,7 @@ type TraceSearcher interface { requires !Matches(snapshot) requires MatchProperties(tr.getPrev(snapshot), entry) ensures MatchProperties(snapshot, entry) - MatchPropertiesTransitive(snapshot, entry tr.TraceEntry) + MatchPropertiesTransitive(ghost snapshot, entry tr.TraceEntry) ghost decreases @@ -106,7 +106,7 @@ type TraceSearcher interface { * entry will occur further in the trace's past. This then also implies that we * cannot have reached the root yet */ - OccursImpliesAnEventualMatch(entry tr.TraceEntry) + OccursImpliesAnEventualMatch(ghost entry tr.TraceEntry) ghost decreases @@ -120,7 +120,7 @@ type TraceSearcher interface { * pure component of the `validTrace` invariant that belongs to the entry that * was searched. */ - ExtractPureEntryInv(entry tr.TraceEntry, p perm) + ExtractPureEntryInv(ghost entry tr.TraceEntry, ghost p perm) } ghost @@ -143,7 +143,7 @@ ensures acc(tri.validTrace(searcher.Ctx(), prev), p) --* acc(tri.validTrace(sea * Searches on the trace for an existing entry and returns this entry. * Furthermore, the (impure) valid trace invariant at the time point back then is returned. */ -func (m *TraceManager) findEntryWithInv(searcher TraceSearcher, validTraceEntry, entry tr.TraceEntry, p perm) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) findEntryWithInv(searcher TraceSearcher, validTraceEntry, entry tr.TraceEntry, p perm) (prev tr.TraceEntry) { ctx := searcher.Ctx() if validTraceEntry == entry { unfold acc(tri.validTrace(ctx, validTraceEntry), p) @@ -191,7 +191,7 @@ ensures m.ImmutableState(searcher.Ctx(), owner) == old(m.ImmutableState(searche * Searches on the trace for an existing entry and returns this entry. * Furthermore, the pure invariant for the located entry is returned. */ -func (m *TraceManager) findEntryWithPureInv(searcher TraceSearcher, owner Client) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) findEntryWithPureInv(searcher TraceSearcher, owner Client) (prev tr.TraceEntry) { prev = m.findEntryWithPureInvWithSnap(searcher, owner, m.Snapshot(searcher.Ctx(), owner)) } @@ -211,7 +211,7 @@ ensures m.ImmutableState(searcher.Ctx(), owner) == old(m.ImmutableState(searche * Searches on the trace for an existing entry and returns this entry. * Furthermore, the pure invariant for the located entry is returned. */ -func (m *TraceManager) findEntryWithPureInvWithSnap(searcher TraceSearcher, owner Client, snap tr.TraceEntry) (prev tr.TraceEntry) { +func (m gpointer[TraceManager]) findEntryWithPureInvWithSnap(searcher TraceSearcher, owner Client, snap tr.TraceEntry) (prev tr.TraceEntry) { // to obtain the validTrace predicate instance, we have to aquire the lock and apply monotonicity: lastSeenSnapshot, snapshot := m.acquireValidTrace(searcher.Ctx(), owner) snap.isSuffixTransitive(lastSeenSnapshot, snapshot) @@ -253,7 +253,7 @@ ensures s1 != s2 ==> localValidTrace(searcher2.Ctx(), s2) && ((localValidTrace(searcher1.Ctx(), s1) && localValidTrace(searcher2.Ctx(), s2)) --* tri.validTrace(searcher1.Ctx(), validTraceEntry)) // this lemma is part of the manager as it requires the validTrace predicate -func (m *TraceManager) findEntriesWithInv(searcher1, searcher2 TraceSearcher, validTraceEntry tr.TraceEntry) (s1, s2 tr.TraceEntry) { +func (m gpointer[TraceManager]) findEntriesWithInv(searcher1, searcher2 TraceSearcher, validTraceEntry tr.TraceEntry) (s1, s2 tr.TraceEntry) { ctx := searcher1.Ctx() s1Found := false s2Found := false diff --git a/usage/usage.gobra b/usage/usage.gobra index 3c3ab83..1e19455 100644 --- a/usage/usage.gobra +++ b/usage/usage.gobra @@ -1,7 +1,7 @@ package usage -type Usage domain { +ghost type Usage domain { // constructors // type 0 func PkeKey(string) Usage diff --git a/usagecontext/usage-context.gobra b/usagecontext/usage-context.gobra index dcc49ce..aad20f5 100644 --- a/usagecontext/usage-context.gobra +++ b/usagecontext/usage-context.gobra @@ -5,43 +5,43 @@ import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace" import u "github.com/ModularVerification/ReusableVerificationLibrary/usage" -type UsageOption = option[u.Usage] +ghost type UsageOption = option[u.Usage] type UsageContext interface { ghost decreases - pure GetUsage(t tm.Term) UsageOption + pure GetUsage(ghost t tm.Term) (ghost res UsageOption) ghost decreases - pure PkePred(t tr.TraceEntry, usageString string, plaintext, pk tm.Term) bool + pure PkePred(ghost t tr.TraceEntry, usageString string, ghost plaintext, pk tm.Term) bool ghost decreases requires t1.isSuffix(t2) requires PkePred(t1, usageString, plaintext, pk) ensures PkePred(t2, usageString, plaintext, pk) - PkePredMonotonic(t1, t2 tr.TraceEntry, usageString string, plaintext, pk tm.Term) + PkePredMonotonic(ghost t1, t2 tr.TraceEntry, usageString string, ghost plaintext, pk tm.Term) ghost decreases - pure AeadPred(t tr.TraceEntry, usageString string, key, nonce, plaintext, authtext tm.Term) bool + pure AeadPred(ghost t tr.TraceEntry, usageString string, ghost key, nonce, plaintext, authtext tm.Term) bool ghost decreases requires t1.isSuffix(t2) requires AeadPred(t1, usageString, key, nonce, plaintext, authtext) ensures AeadPred(t2, usageString, key, nonce, plaintext, authtext) - AeadPredMonotonic(t1, t2 tr.TraceEntry, usageString string, key, nonce, plaintext, authtext tm.Term) + AeadPredMonotonic(ghost t1, t2 tr.TraceEntry, usageString string, ghost key, nonce, plaintext, authtext tm.Term) ghost decreases - pure SignPred(t tr.TraceEntry, usageString string, msg, sk tm.Term) bool + pure SignPred(ghost t tr.TraceEntry, usageString string, ghost msg, sk tm.Term) bool ghost decreases requires t1.isSuffix(t2) requires SignPred(t1, usageString, msg, sk) ensures SignPred(t2, usageString, msg, sk) - SignPredMonotonic(t1, t2 tr.TraceEntry, usageString string, msg, sk tm.Term) + SignPredMonotonic(ghost t1, t2 tr.TraceEntry, usageString string, ghost msg, sk tm.Term) } From a212224c00225b95c6603953513cb23bf95334f1 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 6 Mar 2025 16:15:57 +0100 Subject: [PATCH 2/3] removes CI for GitLab --- .gitlab-ci.yml | 14 -------------- 1 file changed, 14 deletions(-) delete mode 100644 .gitlab-ci.yml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml deleted file mode 100644 index 17b7f12..0000000 --- a/.gitlab-ci.yml +++ /dev/null @@ -1,14 +0,0 @@ -image: - # name: ghcr.io/viperproject/gobra:latest - name: ghcr.io/viperproject/gobra@sha256:432559ae1ea823d612e28f7e5798f1923cf7f4e343040359575c33ae081a01d9 # Gobra commit ab5ab7f - # override entrypoint such that we get a shell in the image - # as the image would otherwise expect a path to a Gobra file - entrypoint: [""] - -verify: - script: - - ./verify.sh - artifacts: - when: always - paths: - - .gobra/stats.json From 6255732283de56b72dbb498690d4fb4c53c015f6 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 6 Mar 2025 18:05:01 +0100 Subject: [PATCH 3/3] fixes missing comment end --- labeledlibrary/crypto.go | 1 + 1 file changed, 1 insertion(+) diff --git a/labeledlibrary/crypto.go b/labeledlibrary/crypto.go index 365acf0..64a683e 100644 --- a/labeledlibrary/crypto.go +++ b/labeledlibrary/crypto.go @@ -235,6 +235,7 @@ func (l *LabeledLibrary) AttackerDec(ciphertext, sk lib.ByteString, ciphertextT } return } +@*/ //@ requires l.Mem() //@ requires acc(lib.Mem(key), 1/16) && acc(lib.Mem(nonce), 1/16)