Code

feat: formal verification#5

Code

Merged

bittermandel merged 30 commits intomainmolnett/valv:mainfrom verificationmolnett/valv:verificationCopy head branch name to clipboardOct 2, 2024

+1,436

Commits

Commits on Oct 2, 2024

• Simple model of encryption and communication user <-> keystore, 3 assertions all passing

  

  kibasaur

  authored and

  bittermandel

  committed
  cc81bd5

  Copy full SHA for cc81bd5

• Changed Markdown

  

  kibasaur

  authored and

  bittermandel

  committed
  019ad4d

  Copy full SHA for 019ad4d

• Added Access Control Component

  

  kibasaur

  authored and

  bittermandel

  committed
  8ad6886

  Copy full SHA for 8ad6886

• Fixed indexation error in Access Control - Decrypt

  

  kibasaur

  authored and

  bittermandel

  committed
  951bc6d

  Copy full SHA for 951bc6d

• database component created, support for additional user in the works, one assertion violated atm

  

  kibasaur

  authored and

  bittermandel

  committed
  699ff68

  Copy full SHA for 699ff68

• assertion violation fixed

  

  kibasaur

  authored and

  bittermandel

  committed
  648295b

  Copy full SHA for 648295b

• KMS now delegates KEKs to tenants. Added alternative clock component. Added assigned_to field to keys. Need to delegate assignment next.

  

  kibasaur

  authored and

  bittermandel

  committed
  5abd84a

  Copy full SHA for 5abd84a

• User changed to Tenant

  

  kibasaur

  authored and

  bittermandel

  committed
  019cd03

  Copy full SHA for 019cd03

• Model is mostly done with an alternative model that only uses a single KEK in the system.

  

  kibasaur

  authored and

  bittermandel

  committed
  43bd627

  Copy full SHA for 43bd627

• removed some global vars

  

  kibasaur

  authored and

  bittermandel

  committed
  323a3f5

  Copy full SHA for 323a3f5

• changed process id check to simply passed id parameter in proctype Tenant()

  

  kibasaur

  authored and

  bittermandel

  committed
  ede879b

  Copy full SHA for ede879b

• Formatting and edited comments

  

  kibasaur

  authored and

  bittermandel

  committed
  fd161d3

  Copy full SHA for fd161d3

• Added some information in README.md

  

  kibasaur

  authored and

  bittermandel

  committed
  9dddc38

  Copy full SHA for 9dddc38

• Formatting in README.md

  

  kibasaur

  authored and

  bittermandel

  committed
  f21e16d

  Copy full SHA for f21e16d

• Reduced memory usage significantly

  

  kibasaur

  authored and

  bittermandel

  committed
  f765133

  Copy full SHA for f765133

• New model_c which is asynch and can handle 2 requests and be run in about 30 minutes

  

  kibasaur

  authored and

  bittermandel

  committed
  5e0a755

  Copy full SHA for 5e0a755

• Safety v1 for model 1 verified

  

  kibasaur

  authored and

  bittermandel

  committed
  95f62a1

  Copy full SHA for 95f62a1

• model_c contains assign, encrypt and decrypt and ready to be verified. Recrypt to be finalized as well as decryption with grant.

  Show description for abd6dab
  

  kibasaur

  authored and

  bittermandel

  committed
  abd6dab

  Copy full SHA for abd6dab

• changes weren't added to model_c, so recommit

  

  kibasaur

  authored and

  bittermandel

  committed
  1c7ddaa

  Copy full SHA for 1c7ddaa

• Refactored model_c and renamed it model.pml

  

  kibasaur

  authored and

  bittermandel

  committed
  72dac4f

  Copy full SHA for 72dac4f

• Models A-D verified

  

  kibasaur

  authored and

  bittermandel

  committed
  f31e139

  Copy full SHA for f31e139

• Verified

  

  kibasaur

  authored and

  bittermandel

  committed
  4d4dbb1

  Copy full SHA for 4d4dbb1

• edited README

  

  kibasaur

  authored and

  bittermandel

  committed
  91b9e02

  Copy full SHA for 91b9e02

• typo in README

  

  kibasaur

  authored and

  bittermandel

  committed
  5187adc

  Copy full SHA for 5187adc

• changed names of liveness claims

  

  kibasaur

  authored and

  bittermandel

  committed
  00b7f20

  Copy full SHA for 00b7f20

• model 2 and 4 reverified

  

  kibasaur

  authored and

  bittermandel

  committed
  603ce57

  Copy full SHA for 603ce57

• Message vocabulary changed, cache exclusive or added, keystore database step edited

  

  kibasaur

  authored and

  bittermandel

  committed
  5fbdff6

  Copy full SHA for 5fbdff6

• added some documentation to README

  

  kibasaur

  authored and

  bittermandel

  committed
  4c39bfe

  Copy full SHA for 4c39bfe

• fix: this file shouldnt be committed

  bittermandel

  committed
  a829f47

  Copy full SHA for a829f47

• docs: rename and correction of docs

  bittermandel

  committed
  614d3e5

  Copy full SHA for 614d3e5