Skip to content

Commit

Permalink
chore: use built-in SAT solver for CBMC proofs
Browse files Browse the repository at this point in the history
Invoking an external solver is not necessarily cheaper in terms of CPU
or memory usage.
  • Loading branch information
tautschnig committed Apr 25, 2024
1 parent cb22f6a commit 70d34ab
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 3 deletions.
2 changes: 0 additions & 2 deletions .github/workflows/proof_ci.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -152,8 +152,6 @@ jobs:
echo "$(pwd)" >> $GITHUB_PATH
- name: Run CBMC proofs
shell: bash
env:
EXTERNAL_SAT_SOLVER: kissat
working-directory: ${{ env.PROOFS_DIR }}
run: ${{ env.RUN_CBMC_PROOFS_COMMAND }}
- name: Check repository visibility
Expand Down
2 changes: 1 addition & 1 deletion aws-encryption-sdk-specification
Submodule aws-encryption-sdk-specification updated 93 files
+0 −5 .github/CODEOWNERS
+0 −4 .github/PULL_REQUEST_TEMPLATE.md
+1 −1 .github/workflows/ci_static-analysis.yaml
+1 −7 .gitignore
+0 −2 .prettierignore
+0 −91 README.md
+1 −1 changes/2020-05-13_remove-keyring-trace/change.md
+8 −8 changes/2020-06-09_wrapping-key-identifiers/change.md
+0 −301 changes/2022-06-19_seperate_material_providers/background.md
+0 −130 changes/2022-06-19_seperate_material_providers/change.md
+0 −441 changes/2022-11-14_encryption_context_on_decrypt/background.md
+0 −259 changes/2022-11-14_encryption_context_on_decrypt/encryption_context_use_cases.md
+0 −360 changes/2022-11-14_encryption_context_on_decrypt/proposal.md
+0 −217 changes/2023-06-19_thread_safe_cache/background.md
+0 −196 changes/2023-06-19_thread_safe_cache/change.md
+0 −286 changes/2023_7_12_update-keystore-structure/background.md
+0 −150 changes/2023_7_12_update-keystore-structure/proposal.md
+1 −1 ci/prettify.sh
+0 −100 client-apis/client.md
+9 −58 client-apis/decrypt.md
+31 −94 client-apis/encrypt.md
+178 −0 compliance/framework/aws-kms/aws-kms-key-arn.txt
+79 −0 compliance/framework/aws-kms/aws-kms-key-arn/2.5.toml
+47 −0 compliance/framework/aws-kms/aws-kms-key-arn/2.8.toml
+52 −0 compliance/framework/aws-kms/aws-kms-key-arn/2.9.toml
+123 −0 compliance/framework/aws-kms/aws-kms-mrk-are-unique.txt
+48 −0 compliance/framework/aws-kms/aws-kms-mrk-are-unique/2.5.toml
+233 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider.txt
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.5.toml
+102 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.6.toml
+182 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.7.toml
+50 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.8.toml
+106 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.9.toml
+225 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key.txt
+81 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.10.toml
+63 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.11.toml
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.5.toml
+64 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.6.toml
+12 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.7.toml
+12 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.8.toml
+179 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.9.toml
+194 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings.txt
+98 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings/2.5.toml
+163 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings/2.6.toml
+311 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.5.toml
+42 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.6.toml
+258 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.7.toml
+217 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.8.toml
+212 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring.txt
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.5.toml
+61 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.6.toml
+12 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.7.toml
+258 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.8.toml
+110 −0 compliance/framework/aws-kms/aws-kms-mrk-match-for-decrypt.txt
+48 −0 compliance/framework/aws-kms/aws-kms-mrk-match-for-decrypt/2.5.toml
+3 −1 data-format/message-body.md
+46 −68 data-format/message-header.md
+1 −4 data-format/message.md
+0 −44 framework/README.md
+89 −449 framework/algorithm-suites.md
+0 −112 framework/aws-kms/aws-kms-discovery-keyring.md
+0 −403 framework/aws-kms/aws-kms-hierarchical-keyring.md
+0 −166 framework/aws-kms/aws-kms-keyring.md
+30 −29 framework/aws-kms/aws-kms-mrk-aware-multi-keyrings.md
+36 −36 framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.md
+20 −20 framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring.md
+1 −1 framework/aws-kms/aws-kms-mrk-match-for-decrypt.md
+0 −109 framework/aws-kms/aws-kms-multi-keyrings.md
+0 −267 framework/aws-kms/aws-kms-rsa-keyring.md
+0 −636 framework/branch-key-store.md
+4 −3 framework/caching-cmm.md
+8 −57 framework/cmm-interface.md
+0 −110 framework/commitment-policy.md
+13 −91 framework/cryptographic-materials-cache.md
+25 −48 framework/default-cmm.md
+24 −41 framework/keyring-interface.md
+395 −0 framework/kms-keyring.md
+16 −10 framework/local-cryptographic-materials-cache.md
+12 −9 framework/multi-keyring.md
+24 −35 framework/raw-aes-keyring.md
+6 −6 framework/raw-rsa-keyring.md
+0 −104 framework/required-encryption-context-cmm.md
+0 −162 framework/storm-tracking-cryptographic-materials-cache.md
+8 −239 framework/structures.md
+0 −38 framework/synchronized-local-cryptographic-materials-cache.md
+0 −113 framework/transitive-requirements.md
+0 −0 proposals/2020-07-01_aws-kms-keyring-redesign/background.md
+3 −3 proposals/2020-07-01_aws-kms-keyring-redesign/change.md
+0 −68 proposals/2022-10-27_rsa-keyring-v2/proposal.md
+12 −20 util/extract.js
+1 −1 util/report.js
+0 −17 util/specification_extract.sh

0 comments on commit 70d34ab

Please sign in to comment.