Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add SAW proofs for integration of Arm proofs for SHA384 #128

Merged
merged 7 commits into from
Dec 6, 2023

Conversation

pennyannn
Copy link
Contributor

@pennyannn pennyannn commented Nov 30, 2023

This PR extends existing SHA384/512 proofs to support Arm LLVM IR. This work fulfills the integration of Arm assembly proofs in #122 .

Specifically, this PR:

  1. Adds a new workflow called SAW_aarch64 that compiles aws-lc to AArch64 LLVM IR and run SHA384 proofs with the AAarch64 LLVM IR
  2. The SAW proofs are refactored to two sets of proofs:
  • For X86_64: verify-SHA384-x86.saw and verify-SHA512-x86.saw
  • For AAarch64: verify-SHA384-aarch64-neoverse-n1.saw, verify-SHA384-aarch64-neoverse-v1.saw, verify-SHA512-aarch64-neoverse-n1.saw and verify-SHA512-aarch64-neoverse-v1.saw (currently SHA512 proofs are disabled due to a safety check issue)
  1. A set of shell scripts are written to support the workflow

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

@pennyannn pennyannn force-pushed the yppe/arm-integration-saw branch 11 times, most recently from 2ea23fa to dd5724f Compare November 30, 2023 20:26
@pennyannn pennyannn force-pushed the yppe/arm-integration-saw branch 3 times, most recently from 9436a9c to dd0325f Compare November 30, 2023 20:59
@pennyannn pennyannn marked this pull request as ready for review November 30, 2023 21:03
@pennyannn pennyannn force-pushed the yppe/arm-integration-saw branch 6 times, most recently from 31cf9a1 to e3e9eb5 Compare December 1, 2023 01:50
@pennyannn pennyannn force-pushed the yppe/arm-integration-saw branch 3 times, most recently from fd357ac to 5bdbff6 Compare December 1, 2023 22:41
@pennyannn pennyannn force-pushed the yppe/arm-integration-saw branch 2 times, most recently from be02daa to dc37624 Compare December 1, 2023 23:55
NSym/spec/SHA384recEquiv.cry Outdated Show resolved Hide resolved
NSym/spec/SHA512recEquiv.cry Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
SAW/proof/SHA512/SHA512-common.saw Show resolved Hide resolved
SAW/proof/common/asm_helpers.saw Outdated Show resolved Hide resolved
@pennyannn pennyannn force-pushed the yppe/arm-integration-saw branch 16 times, most recently from 6dd240c to 6724bc9 Compare December 4, 2023 18:50
README.md Outdated Show resolved Hide resolved
@pennyannn pennyannn merged commit a7affcc into awslabs:master Dec 6, 2023
4 checks passed
@pennyannn pennyannn deleted the yppe/arm-integration-saw branch December 6, 2023 23:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants