Code

Add CN specs to MKM#142

Code

Open

podhrmic wants to merge 42 commits intomainGaloisInc/VERSE-OpenSUT:mainfrom 139-feature-verify-test-mkm-moduleGaloisInc/VERSE-OpenSUT:139-feature-verify-test-mkm-moduleCopy head branch name to clipboard

+815-93

Commits

Commits on Dec 18, 2024

• add client-reduced, update cn_stubs

  septract

  committed
  218a2f2

  Copy full SHA for 218a2f2

Commits on Dec 19, 2024

• Migrate CN memory safety specs into client.c

  septract

  committed
  405d646

  Copy full SHA for 405d646

Commits on Dec 20, 2024

• mkm: Prove memory safety for remaining fns

  septract

  committed
  de0ba91

  Copy full SHA for de0ba91

• mkm: make proof use CN standard predicates

  septract

  committed
  4f4b81e

  Copy full SHA for 4f4b81e

Commits on Dec 21, 2024

• mkm: handle array slices properly in read/write

  septract

  committed
  f2cb2d9

  Copy full SHA for f2cb2d9

• Remove old test file client-reduced.c

  septract

  committed
  c7f87d3

  Copy full SHA for c7f87d3

• mkm: add state machine to client_event spec

  septract

  committed
  093dd29

  Copy full SHA for 093dd29

• mkm: guard CN-specific ghost code with a macro

  septract

  committed
  b7c4a19

  Copy full SHA for b7c4a19

Commits on Dec 27, 2024

• mkm: clean up proof

  septract

  committed
  faaa2ef

  Copy full SHA for faaa2ef

• mkm: add script to split files, make client.h and others work with it

  septract

  committed
  6fa262f

  Copy full SHA for 6fa262f

Commits on Dec 28, 2024

• mkm: Add test script for cn test, modify other files to make it work

  septract

  committed
  b50dd49

  Copy full SHA for b50dd49

• mkm: minor proof cleanup

  septract

  committed
  6a59c43

  Copy full SHA for 6a59c43

Commits on Dec 31, 2024

• mkm: make cn test work for most of the mkm fns

  septract

  committed
  c520554

  Copy full SHA for c520554

• mkm: minor proof tidy up

  septract

  committed
  adb30eb

  Copy full SHA for adb30eb

• mkm: made testing work with malloc / free fns, various cleanup

  septract

  committed
  e0f081f

  Copy full SHA for e0f081f

Commits on Jan 1, 2025

• mkm: integrated possibly-failing malloc()

  septract

  committed
  8466469

  Copy full SHA for 8466469

Commits on Jan 3, 2025

• mkm: fix test demo pauses, support can-fail malloc in cn test flow

  septract

  committed
  c44975b

  Copy full SHA for c44975b

• mkm: test script now needs legacy --with-static-hack flag

  septract

  committed
  59e7337

  Copy full SHA for 59e7337

• mkm: match Rust Option type naming

  septract

  committed
  aa65423

  Copy full SHA for aa65423

Commits on Jan 5, 2025

• mkm: use default in definitions (depends on cerberus PR #814)

  septract

  committed
  a55fcb5

  Copy full SHA for a55fcb5

Commits on Jan 7, 2025

• mkm: initial work verifying policy.c

  septract

  committed
  c8c7d93

  Copy full SHA for c8c7d93

Commits on Jan 16, 2025

• Add testing to CI job

  septract

  committed
  2d49909

  Copy full SHA for 2d49909

• mps: add mkm proof GH action

  septract

  committed
  bdcb111

  Copy full SHA for bdcb111

• mkm: fix typo, add cn test workflow

  septract

  committed
  1a75a5b

  Copy full SHA for 1a75a5b

• mkm: Address @podhrmic comments

  septract

  committed
  e9e6211

  Copy full SHA for e9e6211

Commits on Jan 18, 2025

• mkm: prove / test functions in policy.c modulo hacks

  septract

  committed
  76862a7

  Copy full SHA for 76862a7

Commits on Jan 31, 2025

• Do not use stdio in cn exec

  Show description for 7696586
  peterohanley

  committed
  7696586

  Copy full SHA for 7696586

• Disable the struct definition only in cn exec

  peterohanley

  committed
  35fbced

  Copy full SHA for 35fbced

• mkm: uncomment hmac call in policy.c

  spernsteiner

  committed
  53495b1

  Copy full SHA for 53495b1

Commits on Feb 7, 2025

• Fix frama-c proofs

  podhrmic

  committed
  625ec77

  Copy full SHA for 625ec77

• install missing deps in frama-c image

  podhrmic

  committed
  702f5ca

  Copy full SHA for 702f5ca

• Try different way of writing the steps

  podhrmic

  committed
  249d53d

  Copy full SHA for 249d53d

• Try to debug the frama-c invocation

  podhrmic

  committed
  022142e

  Copy full SHA for 022142e

• Fix path

  podhrmic

  committed
  bdd35b7

  Copy full SHA for bdd35b7

• Skip docker-run action

  podhrmic

  committed
  60d8f1f

  Copy full SHA for 60d8f1f

• Fix container definition:

  podhrmic

  committed
  d0e7057

  Copy full SHA for d0e7057

• Revert the frama-c job changes

  podhrmic

  committed
  f5b0dab

  Copy full SHA for f5b0dab

• Install frama-C from a distro package

  podhrmic

  committed
  ead7d69

  Copy full SHA for ead7d69

• Revert frama-c job to what is in main

  podhrmic

  committed
  a153764

  Copy full SHA for a153764

• Switch to a different docker-run action

  podhrmic

  committed
  43f3033

  Copy full SHA for 43f3033

Commits on Feb 11, 2025

• mkm: resolved TODOs or converted to NOTE

  septract

  committed
  f9aaeeb

  Copy full SHA for f9aaeeb

• One more TODO

  septract

  committed
  bc27384

  Copy full SHA for bc27384