adds full source code

README.md

@@ -1,13 +1,9 @@
-# Thesis Template
-
-[![build status](/../badges/master/build.svg)](/../commits/master)
-
-Quick links:
-
-*   [Download](/../-/jobs/artifacts/master/raw/description/description.pdf?job=build) project description.
-*   [Download](/../-/jobs/artifacts/master/raw/report/thesis.pdf?job=build) thesis report.
-
-Welcome! This repository contains templates for the project
-[description](description) and [report](report) (taken from
-[here](https://www.cadmo.ethz.ch/education/thesis/template.html)). Feel
-free to adapt them to your needs. 
+# Secure Deletion of Sensitive Data in Protocol Implementations
+**Hugo Queinnec, 2023**
+
+This repo contains the source code associated to this Master's thesis, as well as the Latex source files of the project description and the final report.
+It is organized as follows:
+- [`library`](./library/) contains the source code of the extended Reusable Verification Library in Go.
+- [`ratcheting-protocol`](./ratcheting-protocol) contains the source code of the full ratcheting protocol implementation (and specification) in Go. As explained in the report, this implementation is not yet complete.
+- [`report`](./report/) contains the Latex source files of the final report.
+- [`description`](./description/) contains the Latex source files of the project description.

library/.gitignore

@@ -0,0 +1,4 @@
+.DS_Store
+tmp/
+logger.log
+.gobra/

library/.verification/crypto/rand/rand.gobra

@@ -0,0 +1,4 @@
+package rand
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/crypto/rsa/rsa.gobra

@@ -0,0 +1,4 @@
+package rsa
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/crypto/sha256/sha256.gobra

@@ -0,0 +1,4 @@
+package sha256
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/crypto/x509/x509.gobra

@@ -0,0 +1,4 @@
+package x509
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/encoding/hex/hex.gobra

@@ -0,0 +1,4 @@
+package hex
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/golang.org/x/crypto/chacha20poly1305/chacha20poly1305.gobra

@@ -0,0 +1,4 @@
+package chacha20poly1305
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/golang.org/x/crypto/nacl/sign/sign.gobra

@@ -0,0 +1,4 @@
+package sign
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/io/io.gobra

@@ -0,0 +1,4 @@
+package io
+
+// empty but necessary since Gobra needs all transitively imported packages
+// to perform the global variable analysis

library/.verification/math/big/big.gobra

@@ -0,0 +1,5 @@
+package big
+
+type Int struct {
+    nonEmptyStruct int
+}

library/arbitrary/arbitrary.gobra

@@ -0,0 +1,48 @@
+package arbitrary
+
+import ev "github.com/ModularVerification/ReusableVerificationLibrary/event"
+import "github.com/ModularVerification/ReusableVerificationLibrary/label"
+import p "github.com/ModularVerification/ReusableVerificationLibrary/principal"
+import tm "github.com/ModularVerification/ReusableVerificationLibrary/term"
+import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace"
+import u "github.com/ModularVerification/ReusableVerificationLibrary/usage"
+
+// utility package to return an arbitrary value which can then be used for forall introductions.
+// these Go functions correspond to Viper methods that do not have any postcondition and thus do not constrain
+// their return value.
+
+decreases
+func GetArbTerm() tm.Term
+
+decreases
+func GetArbTraceEntry() tr.TraceEntry
+
+decreases
+func GetArbLabel() label.SecrecyLabel
+
+decreases
+func GetArbPrincipal() p.Principal
+
+decreases
+func GetArbId() p.Id
+
+decreases
+func GetArbEvent() ev.Event
+
+decreases
+func GetArbUsage() u.Usage
+
+decreases
+func GetArbString() string
+
+decreases
+func GetArbUInt32() uint32
+
+decreases
+func GetArbUInt64() uint64
+
+decreases
+func GetArbInt() int
+
+decreases
+func GetArbBool() bool

library/attacker/attacker.gobra

@@ -0,0 +1,33 @@
+package attacker
+
+import tm "github.com/ModularVerification/ReusableVerificationLibrary/term"
+import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace"
+
+ghost
+decreases
+pure func attackerKnows(entry tr.TraceEntry, term tm.Term) bool {
+    return term in attackerKnowledge(entry)
+}
+
+ghost
+decreases
+requires attackerKnows(t1, term)
+requires t1.isSuffix(t2)
+ensures  attackerKnows(t2, term)
+func attackerKnowsMonotonic(t1, t2 tr.TraceEntry, term tm.Term) bool {
+    t1.getPublicTermsMonotonic(t2)
+    t1.getMessagePayloadsMonotonic(t2)
+    t1.getTermsMadePublicMonotonic(t2)
+}
+
+ghost
+decreases
+pure func isUnknownToAttacker(entry tr.TraceEntry, term tm.Term) bool {
+    return !attackerKnows(entry, term)
+}
+
+ghost
+decreases
+pure func attackerKnowledge(entry tr.TraceEntry) set[tm.Term] {
+    return entry.getPublicTerms() union entry.getMessagePayloads() union entry.getTermsMadePublic()
+}

library/attacker/attacker.gobra.gobrafied

@@ -0,0 +1,33 @@
+package attacker
+
+import tm "github.com/ModularVerification/ReusableVerificationLibrary/term"
+import tr "github.com/ModularVerification/ReusableVerificationLibrary/trace"
+
+ghost
+decreases
+pure func attackerKnows(entry tr.TraceEntry, term tm.Term) bool {
+    return term in attackerKnowledge(entry)
+}
+
+ghost
+decreases
+requires attackerKnows(t1, term)
+requires t1.isSuffix(t2)
+ensures  attackerKnows(t2, term)
+func attackerKnowsMonotonic(t1, t2 tr.TraceEntry, term tm.Term) bool {
+    t1.getPublicTermsMonotonic(t2)
+    t1.getMessagePayloadsMonotonic(t2)
+    t1.getTermsMadePublicMonotonic(t2)
+}
+
+ghost
+decreases
+pure func isUnknownToAttacker(entry tr.TraceEntry, term tm.Term) bool {
+    return !attackerKnows(entry, term)
+}
+
+ghost
+decreases
+pure func attackerKnowledge(entry tr.TraceEntry) set[tm.Term] {
+    return entry.getPublicTerms() union entry.getMessagePayloads() union entry.getTermsMadePublic()
+}

library/attacker/attacker.gobra.unparsed

@@ -0,0 +1,33 @@
+package attacker
+
+
+import tm github.com/ModularVerification/ReusableVerificationLibrary/term
+
+import tr github.com/ModularVerification/ReusableVerificationLibrary/trace
+ghost pure
+decreases  
+func attackerKnows(entry tr.TraceEntry, term tm.Term) (bool) {
+  return term in attackerKnowledge(entry)
+}
+
+ghost requires attackerKnows(t1, term)
+requires t1.isSuffix(t2)
+ensures attackerKnows(t2, term)
+decreases  
+func attackerKnowsMonotonic(t1 tr.TraceEntry, t2 tr.TraceEntry, term tm.Term) (bool) {
+  t1.getPublicTermsMonotonic(t2)
+  t1.getMessagePayloadsMonotonic(t2)
+  t1.getTermsMadePublicMonotonic(t2)
+}
+
+ghost pure
+decreases  
+func isUnknownToAttacker(entry tr.TraceEntry, term tm.Term) (bool) {
+  return !attackerKnows(entry, term)
+}
+
+ghost pure
+decreases  
+func attackerKnowledge(entry tr.TraceEntry) (set[tm.Term]) {
+  return entry.getPublicTerms() union entry.getMessagePayloads() union entry.getTermsMadePublic()
+}