project-oak silveroak issues

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.

Apache License 2.0

124 stars 20 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Bump nokogiri from 1.11.5 to 1.13.6 in /docs

#970 dependabot[bot] opened 2 years ago
0
Bump nokogiri from 1.11.5 to 1.13.4 in /docs

#969 dependabot[bot] closed 2 years ago
1
Bump nokogiri from 1.11.5 to 1.13.3 in /docs

#968 dependabot[bot] closed 2 years ago
1
fix typos found by spellchecker

#967 ju-sh closed 2 years ago
1
Fix tiny typo

#966 ju-sh closed 2 years ago
1
Express device_implements_state_machine using only run1, without runUntilResp

#965 fshaked closed 2 years ago
1
Add proof for sha256_len

#964 yanok closed 3 years ago
1
Name the circuit state types (fixes #962)

#963 samuelgruetter closed 3 years ago
0
Modularize circuit state appearing in types

#962 samuelgruetter closed 3 years ago
0
Add HMAC registers to circuit needed by software:

#961 blaxill closed 3 years ago
2
express `device_implements_state_machine` using only `run1`, without `runUntilResp` (on top of #959)

#960 samuelgruetter opened 3 years ago
2
run bedrock2-generated RISC-V code in verilator simulation

#959 samuelgruetter closed 3 years ago
0
Big-step lemmas for invariant framework

#958 jadephilipoom closed 3 years ago
2
Pass arguments in RISC-V argument registers (instead of using hardcoded heap addresses)

#957 samuelgruetter closed 3 years ago
2
Add spec and proof of Hmac Inner block

#956 blaxill closed 3 years ago
5
Relax precondition on SHA256 spec and hotfix for HMAC

#955 blaxill closed 3 years ago
0
Tlul spec (merge after #953)

#954 fshaked closed 3 years ago
0
Add tactic for destructing cava2 states

#953 fshaked closed 3 years ago
0
Finish remaining SHA256 proof items

#952 blaxill closed 3 years ago
1
Example SystemVerilog output from SilverOak stage 1

#951 blaxill opened 3 years ago
0
Partial version of sha256 proof

#948 jadephilipoom closed 3 years ago
2
Add HMAC bypass mode

#947 blaxill closed 3 years ago
1
Use the actual Hmac Cava2 device instead of placeholders

#946 fshaked closed 3 years ago
4
Bump nokogiri from 1.11.5 to 1.12.5 in /docs

#945 dependabot[bot] closed 2 years ago
1
Use invariant classes for components

#944 blaxill closed 3 years ago
1
Add `concat_bytes` & misc. proofs

#943 blaxill closed 3 years ago
1
Change device.run1 to use TL interface

#942 fshaked closed 3 years ago
2
Add is_read to io_req

#941 fshaked closed 3 years ago
0
Add realign_fifo spec and proof

#940 blaxill closed 3 years ago
0
Increment device with TLUL

#939 fshaked closed 3 years ago
0
Adjust sha256_inner proofs

#938 jadephilipoom closed 3 years ago
0
Prove and reorganize all padder helper lemmas

#937 jadephilipoom closed 3 years ago
0
Port existing SHA-256 proofs to new invariant infrastructure

#936 jadephilipoom closed 3 years ago
0
Fix padder proof admits

#935 jadephilipoom closed 3 years ago
0
Add concrete instantiations to abstract example

#934 jadephilipoom closed 3 years ago
0
Add more comparators and fold_left templates

#933 jadephilipoom closed 3 years ago
0
More structured invariant-reasoning infrastructure with examples

#932 jadephilipoom closed 3 years ago
2
Export cava2 library in a few prepackaged files

#931 jadephilipoom opened 3 years ago
0
Realign spec and proofs

#930 blaxill closed 3 years ago
4
Make use of tvar typeclass

#929 jadephilipoom closed 3 years ago
5
Move some lemmas to cava2/ExprProperties.v

#928 jadephilipoom closed 3 years ago
0
I need to know that BitVec's are bounded by 2^n.

#927 fshaked opened 3 years ago
2
Complete padder proofs

#926 jadephilipoom closed 3 years ago
2
Fix padder bug

#925 jadephilipoom closed 3 years ago
0
Partial padder output correctness proof

#924 jadephilipoom closed 3 years ago
0
More progress on padder proofs

#923 jadephilipoom closed 3 years ago
0
Fix bug in SHA-256 padder

#922 jadephilipoom closed 3 years ago
0
WIP invariant and partial proofs for SHA-256 padder

#921 jadephilipoom closed 3 years ago
2
Rename True and False constant circuits to One and Zero

#920 jadephilipoom closed 3 years ago
0
Fifo spec

#919 blaxill closed 3 years ago
5