-
Notifications
You must be signed in to change notification settings - Fork 56
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: backport maintenance/doc changes and prepare release for v1.9.1 (
#731) * Add CBMC CI configuration (#709) This commit adds a configuration file for the "CBMC Proofs" CI check. This is in preparation for adding some custom check-out steps later. * Use private submodules before CI run (#711) * chore: Use continuous-integration environment for private submodule access (#714) Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore: Add support policy (#720) * Upgrade CBMC proof tools: starter kit and Litani 1.10.0 (#722) * Upgrade proof tool submodules This commit advances Litani to release 1.10.0, and the starter kit to the tip-of-tree. This brings the following improvements: - Profiling - Litani measures the memory usage of the CBMC safety checking and coverage checking jobs - The dashboard includes box-and-whisker diagrams for memory use per proof - The dashboard includes a graph of how many parallel jobs are running over the whole run, making it easy to choose a CI machine with enough parallelism - It is now possible to designate particular proofs as "EXPENSIVE"; Litani runs expensive proofs serially, ensuring that they do not over-consume resources like RAM. - UI improvements - Each pipeline page includes a table of contents - Each pipeline page includes a dependency graph of the pipeline - Each job on the pipeline page has a hyperlink to that job - The terminal output is now less noisy * Change cbmc-batch.yaml to cbmc-proof.txt This makes the proof layout consistent with the starter kit, which will allow us to use a generic run script in a future commit. Putting this in commit by itself because the diff is huge and not worth reading (just moving some files and changing two lines in the runscript). * Symlink run-cbmc-proofs.py to starter kit The run script is now a symbolic link into the starter kit submodule, meaning that it will be updated whenever the starter kit is. This is done iso that E-SDK doesn't carry custom modifications to the run script unless necessary; previous commits have made the E-SDK proofs consistent with the generic starter kit conventions. * fix: Simplify / update build instructions. (#713) Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com> * fix(proof_timeout): mark high-memory proofs expensive (#710) * Removed OOM test, as OOM is no longer possible from aws allocators (#728) * chore: pin newer aws-sdk-cpp in macOS CI builds (#729) * chore: update version number and changelog for v1.9.1 * chore: update CBMC CI submodules Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Ben Farley <47006790+farleyb-amazon@users.noreply.github.com> Co-authored-by: lizroth <30636882+lizroth@users.noreply.github.com> Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Justin Boswell <boswej@amazon.com>
- Loading branch information
1 parent
61f4c4c
commit 8254b92
Showing
224 changed files
with
371 additions
and
948 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
Overview | ||
======== | ||
This page describes the support policy for the AWS Encryption SDK. We regularly provide the AWS Encryption SDK with updates that may contain support for new or updated APIs, new features, enhancements, bug fixes, security patches, or documentation updates. Updates may also address changes with dependencies, language runtimes, and operating systems. | ||
|
||
We recommend users to stay up-to-date with Encryption SDK releases to keep up with the latest features, security updates, and underlying dependencies. Continued use of an unsupported SDK version is not recommended and is done at the user’s discretion | ||
|
||
|
||
Major Version Lifecycle | ||
======================== | ||
The AWS Encryption SDK follows the same major version lifecycle as the AWS SDK. For details on this lifecycle, see `AWS SDKs and Tools Maintenance Policy`_. | ||
|
||
Version Support Matrix | ||
====================== | ||
This table describes the current support status of each major version of the AWS Encryption SDK for C. It also shows the next status each major version will transition to, and the date at which that transition will happen. | ||
|
||
.. list-table:: | ||
:widths: 30 50 50 50 | ||
:header-rows: 1 | ||
|
||
* - Major version | ||
- Current status | ||
- Next status | ||
- Next status date | ||
* - 1.x | ||
- Maintenance | ||
- End of Support | ||
- 2022-07-08 | ||
* - 2.x | ||
- Generally Available | ||
- | ||
- | ||
|
||
.. _AWS SDKs and Tools Maintenance Policy: https://docs.aws.amazon.com/sdkref/latest/guide/maint-policy.html#version-life-cycle |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
# Configuration for the "CBMC Proofs" CI | ||
# | ||
# What the CI should do, depending on what branch the pull request | ||
# targets. This is a list of branch names (or '*' as a wildcard that | ||
# matches all branches), with an associated action. Actions can be: | ||
# | ||
# name: run-proofs | ||
# | ||
# or | ||
# | ||
# name: skip | ||
# message: "A message to post to GitHub about why the branch was skipped" | ||
# status: <"success"|"failure"> | ||
# (whether the GitHub status check should succeed or fail) | ||
# | ||
behaviors: | ||
|
||
- target-branches: | ||
- '*' | ||
action: | ||
name: run-proofs | ||
|
||
|
||
checkout-script: | ||
# If this is the private version of the repository, we need to pull in | ||
# the private versions of the submodules. | ||
- "echo Originating GitHub repository: ${GITHUB_REPOSITORY}" | ||
- ./switch-private-submodules --verbose env |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,103 @@ | ||
#!/usr/bin/env python3 | ||
# | ||
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
# | ||
# Licensed under the Apache License, Version 2.0 (the "License"). You | ||
# may not use this file except in compliance with the License. A copy of | ||
# the License is located at | ||
# | ||
# http://aws.amazon.com/apache2.0/ | ||
# | ||
# or in the "license" file accompanying this file. This file is | ||
# distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF | ||
# ANY KIND, either express or implied. See the License for the specific | ||
# language governing permissions and limitations under the License. | ||
|
||
|
||
import argparse | ||
import logging | ||
import os | ||
import subprocess | ||
import sys | ||
|
||
|
||
DESCRIPTION = "Switch between public and private versions of submodules" | ||
|
||
MODULES = [{ | ||
"submodule": "aws-encryption-sdk-cpp/tests/test_vectors/aws-encryption-sdk-test-vectors", | ||
"private": "https://github.com/awslabs/private-aws-encryption-sdk-test-vectors-staging.git", | ||
"public": "https://github.com/awslabs/aws-encryption-sdk-test-vectors.git", | ||
}, { | ||
"submodule": "aws-encryption-sdk-specification", | ||
"private": "https://github.com/awslabs/private-aws-encryption-sdk-specification-staging.git", | ||
"public": "https://github.com/awslabs/aws-encryption-sdk-specification.git", | ||
}] | ||
|
||
|
||
def switch_to(version): | ||
logging.info("Switching to %s version of the submodules", version) | ||
for module in MODULES: | ||
cmd = [ | ||
"git", "config", | ||
f'url."{module[version]}".insteadOf', | ||
module["public"], | ||
] | ||
logging.info(" ".join(cmd)) | ||
subprocess.run(cmd, check=True) | ||
|
||
subprocess.run(["git", "submodule", "sync"], check=True) | ||
subprocess.run([ | ||
"git", "submodule", "update", "--init", "--recursive", "--checkout"], | ||
check=True) | ||
|
||
|
||
def switch_to_env(_): | ||
repo = os.getenv("GITHUB_REPOSITORY") | ||
if not repo: | ||
logging.error( | ||
"Could not determine which submodules to check out " | ||
"($GITHUB_REPOSITORY is not set).") | ||
sys.exit(1) | ||
|
||
if repo == "aws/private-aws-encryption-sdk-c-staging": | ||
switch_to("private") | ||
else: | ||
switch_to("public") | ||
|
||
|
||
OPERATIONS = { | ||
"public": switch_to, | ||
"private": switch_to, | ||
"env": switch_to_env, | ||
} | ||
|
||
|
||
def main(): | ||
pars = argparse.ArgumentParser(description=DESCRIPTION) | ||
for arg in [{ | ||
"flags": ["operation"], | ||
"choices": list(OPERATIONS.keys()), | ||
"default": "public", | ||
"help": "Switch to public or private versions of the submodules, " | ||
"or decide which by reading the $GITHUB_REPOSITORY " | ||
"environment variable. Default: %(default)s." | ||
}, { | ||
"flags": ["-v", "--verbose"], | ||
"action": "store_true", | ||
"help": "verbose output", | ||
}]: | ||
flags = arg.pop("flags") | ||
pars.add_argument(*flags, **arg) | ||
args = pars.parse_args() | ||
|
||
fmt = "switch-private-submodules: %(message)s" | ||
if args.verbose: | ||
logging.basicConfig(format=fmt, level=logging.INFO) | ||
else: | ||
logging.basicConfig(format=fmt, level=logging.WARNING) | ||
|
||
OPERATIONS[args.operation](args.operation) | ||
|
||
|
||
if __name__ == "__main__": | ||
main() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
17 changes: 0 additions & 17 deletions
17
verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
17 changes: 0 additions & 17 deletions
17
verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
17 changes: 0 additions & 17 deletions
17
verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
17 changes: 0 additions & 17 deletions
17
verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
4 changes: 0 additions & 4 deletions
4
verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
4 changes: 0 additions & 4 deletions
4
verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
4 changes: 0 additions & 4 deletions
4
verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
4 changes: 0 additions & 4 deletions
4
verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
4 changes: 0 additions & 4 deletions
4
verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-proof.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
This file marks the directory as containing a CBMC proof |
4 changes: 0 additions & 4 deletions
4
verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-batch.yaml
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.