diff --git a/.github/workflows/osx.yml b/.github/workflows/osx.yml index 53ad7bced..61a329cde 100644 --- a/.github/workflows/osx.yml +++ b/.github/workflows/osx.yml @@ -7,6 +7,7 @@ on: ["pull_request", "push"] jobs: OSX: runs-on: ${{ matrix.os }} + environment: continuous-integration strategy: matrix: @@ -20,13 +21,22 @@ jobs: uses: actions/checkout@v2 with: submodules: recursive + if: ${{ github.repository == 'aws/aws-encryption-sdk-c' }} + + - name: Checkout PR with CI bot token + uses: actions/checkout@v2 + with: + submodules: recursive + token: ${{ secrets.CI_BOT_TOKEN }} + if: ${{ github.repository == 'aws/private-aws-encryption-sdk-c-staging' }} - name: Checkout AWS C++ SDK uses: actions/checkout@v2 with: repository: "aws/aws-sdk-cpp" - ref: "1.8.32" + ref: "1.9.124" path: "aws-sdk-cpp" + submodules: recursive - name: Install dependencies run: diff --git a/CHANGELOG.md b/CHANGELOG.md index aa4d0c37b..1cc4cb5c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,15 @@ # Changelog +## 1.9.1 -- 2021-10-20 + +### Maintenance + +* Add [support policy](/~https://github.com/aws/aws-encryption-sdk-c/blob/master/SUPPORT_POLICY.rst) +* CBMC CI upgrades ([#709](/~https://github.com/aws/aws-encryption-sdk-c/pull/709), [#710](/~https://github.com/aws/aws-encryption-sdk-c/pull/710), [#711](/~https://github.com/aws/aws-encryption-sdk-c/pull/711), [#722](/~https://github.com/aws/aws-encryption-sdk-c/pull/722), [#726](/~https://github.com/aws/aws-encryption-sdk-c/pull/726)) +* Simplify / update build instructions ([#713](/~https://github.com/aws/aws-encryption-sdk-c/pull/713)) +* Remove OOM test, as OOM is no longer possible from aws allocators ([#728](/~https://github.com/aws/aws-encryption-sdk-c/pull/728)) +* Pin newer aws-sdk-cpp in macOS CI builds ([#729](/~https://github.com/aws/aws-encryption-sdk-c/pull/729)) + ## 1.9.0 -- 2021-05-27 * Improvements to the message decryption process. diff --git a/CMakeLists.txt b/CMakeLists.txt index f3e69330d..0a7454a63 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -51,7 +51,7 @@ set(PROJECT_NAME aws-encryption-sdk) # Version number of the SDK to be consumed by C code and Doxygen set(MAJOR 1) set(MINOR 9) -set(PATCH 0) +set(PATCH 1) # Compiler feature tests and feature flags set(USE_ASM TRUE diff --git a/README.md b/README.md index d65df0af8..cc2b92b45 100644 --- a/README.md +++ b/README.md @@ -9,247 +9,126 @@ Also, see the [API documentation](https://aws.github.io/aws-encryption-sdk-c/htm [Security issue notifications](./CONTRIBUTING.md#security-issue-notifications) -## Dependencies +See [Support Policy](./SUPPORT_POLICY.rst) for for details on the current support status of all major versions of this library. -The only direct dependencies of this code are OpenSSL 1.0.2 or higher or 1.1.0 or higher and -[aws-c-common](/~https://github.com/awslabs/aws-c-common) v0.4.42. You will also need -a C compiler and CMake 3.9 or higher. +## Building the AWS Encryption SDK for C with support for AWS KMS -To integrate with [KMS](https://aws.amazon.com/kms/) the AWS Encryption SDK for C also requires -the [AWS SDK for C++](/~https://github.com/aws/aws-sdk-cpp), a C++ compiler, and libcurl. +We will demonstrate some simple build recipes for Linux, Mac, and Windows operating systems. These +recipes assume a newly installed system with default installs of dependency packages. -For best results when doing a build with KMS integration, do not install aws-c-common directly. -Build and install the AWS SDK for C++, which will build and install aws-c-common for you (see the C++ SDK dependancies +The Windows instructions install everything in your current directory (where you run the build process). To change the installation directory, see the Tips and Tricks section at the end of this README. + +The AWS Encryption SDK for C can be used with AWS KMS, but it is not required. If you want to build +a minimal version of the ESDK without AWS KMS support, see "Minimal C build without AWS KMS support", below. + +For best results when doing a build with AWS KMS integration, do not install aws-c-common directly. +Build and install the AWS SDK for C++, which will build and install aws-c-common for you (see the C++ SDK dependencies [here](/~https://github.com/aws/aws-sdk-cpp/blob/master/third-party/CMakeLists.txt#L18)). If you install aws-c-common before building the AWS SDK for C++, this will fool the AWS SDK for C++ install logic, and you will be forced to install several other dependencies manually. Version 1.8.32 of the AWS SDK for C++ is supported by version v1.0.1 of the AWS Encryption SDK for C. -You need to compile both the AWS Encryption SDK for C and its dependencies as either all -shared or all static libraries. We will use all shared library builds in our examples by -using the cmake argument `-DBUILD_SHARED_LIBS=ON`. You can change them to static library -builds by just changing `ON` to `OFF`. - -Once you have built each dependency, install it so it can be picked up by the next build. - ### If you are working on an EC2 instance, regardless of operating system For best results, create an EC2 instance with an instance profile that at a -minimum has KMS permissions for Encrypt, Decrypt, and GenerateDataKey for -at least one KMS CMK in your account. You will not need any other AWS +minimum has AWS KMS permissions for Encrypt, Decrypt, and GenerateDataKey for +at least one KMS key in your account. You will not need any other AWS permissions to use the AWS Encryption SDK for C. -## Build recipes - -We will demonstrate some simple build recipes for Linux, Mac, and Windows operating systems. - -The Linux and Mac recipes install everything in the standard directories in /usr/local. The -Windows recipe installs everything in an install directory placed at the directory you are in -when you start the build process. To change the installation directory, if desired, see the Tips -and Tricks section at the end of this README. - -You can do (Option 1) a C and C++ build, which will include integration with KMS, or you can do -(Option 2) a C only build, which will not include integration with KMS. In places where -the recipes diverge, these will be labeled as (Option 1) and (Option 2). Follow one of the two -options, but not both, depending on which installation you want to do. - -### Building on Amazon Linux - -This recipe should work with a brand new Amazon Linux instance. Start in the directory where -you want to do your build. - -#### Amazon Linux: (Option 1) C and C++ build dependencies - -Run the following: - - sudo yum update - sudo yum install -y openssl-devel git gcc-c++ libcurl-devel - -The yum repo has an old version of CMake, so download CMake 3.9 or later from [their -website](https://cmake.org/) and make sure cmake is in your path. - -Both aws-sdk-cpp and aws-c-common are required, but the installation of aws-sdk-cpp will install -aws-c-common for you. - -Do a KMS-only build of the AWS SDK for C++. If you want to use the AWS SDK for C++ for -other AWS services, you can omit the `-DBUILD_ONLY="kms"` argument, but the build will take much longer. - - git clone /~https://github.com/aws/aws-sdk-cpp.git - mkdir build-aws-sdk-cpp && cd build-aws-sdk-cpp - cmake -DBUILD_SHARED_LIBS=ON -DBUILD_ONLY="kms" -DENABLE_UNITY_BUILD=ON ../aws-sdk-cpp - make && sudo make install ; cd .. - -Now skip to the "Amazon Linux: Build and install the AWS Encryption SDK for C" section below. - -#### Amazon Linux: (Option 2) C only build dependencies - -Run the following: - - sudo yum update - sudo yum install -y openssl-devel git gcc - -The yum repo has an old version of CMake, so download CMake 3.9 or later from [their -website](https://cmake.org/) and make sure cmake is in your path. - -Now build and install aws-c-common: - - git clone /~https://github.com/awslabs/aws-c-common.git - mkdir build-aws-c-common && cd build-aws-c-common - cmake -DBUILD_SHARED_LIBS=ON ../aws-c-common - make && sudo make install ; cd .. - -#### Amazon Linux: Build and install the AWS Encryption SDK for C - - git clone /~https://github.com/aws/aws-encryption-sdk-c.git - mkdir build-aws-encryption-sdk-c && cd build-aws-encryption-sdk-c - cmake -DBUILD_SHARED_LIBS=ON ../aws-encryption-sdk-c - make && sudo make install ; cd .. +### Dependencies -You have successfully built and installed the AWS Encryption SDK for C. +1. OpenSSL 1.0.2 or newer, or 1.1.0 or newer +1. CMake 3.9 or newer +1. C/C++ compiler +1. aws-c-common, typically bundled with the AWS SDK for C++ +1. The AWS SDK for C++ version 1.9.35 or newer -### Building on Ubuntu +The AWS SDK for C++ and the AWS Encryption SDK for C share dependencies on OpenSSL, aws-c-common, and CMake. The AWS SDK for C++ has additional dependencies and prerequisites. See [AWS SDK for +C++: Getting Started](/~https://github.com/aws/aws-sdk-cpp#getting-started). -These instructions have been tested on brand new Ubuntu EC2 instances. You should also -be able to build on Ubuntu operating systems that are not in EC2, but you will need to -manually configure AWS credentials if you are using KMS. Start in the directory where -you want to do your build. +You need to compile the AWS Encryption SDK for C and its dependencies as either all +shared or all static libraries. -#### Ubuntu: (Option 1) C and C++ build dependencies +To build shared libraries, specify the `-DBUILD_SHARED_LIBS=ON` flag to build +aws-c-common, the AWS SDK for C++, and the AWS Encryption SDK. - sudo apt-get update - sudo apt-get install -y libssl-dev cmake g++ libcurl4-openssl-dev zlib1g-dev +To build static libraries, specify the `-DBUILD_SHARED_LIBS=OFF` flag to build +aws-c-common, the AWS SDK for C++, and the AWS Encryption SDK. -Both aws-sdk-cpp and aws-c-common are required, but the installation of aws-sdk-cpp will install -aws-c-common for you. - -Do a KMS-only build of the AWS SDK for C++. If you want to use the AWS SDK for C++ for -other AWS services, you can omit the `-DBUILD_ONLY="kms"` argument, but the build will take much longer. - - git clone /~https://github.com/aws/aws-sdk-cpp.git - mkdir build-aws-sdk-cpp && cd build-aws-sdk-cpp - cmake -DBUILD_SHARED_LIBS=ON -DBUILD_ONLY="kms" -DENABLE_UNITY_BUILD=ON ../aws-sdk-cpp - make && sudo make install ; cd .. +### Linux Build Recipe -Now skip to the "Ubuntu: Build and install the AWS Encryption SDK for C" section below. +First, build the AWS SDK for C++. That will install the shared dependencies. -#### Ubuntu: (Option 2) C only build dependencies +If you only need AWS SDK for C++ to use the AWS Encryption SDK, you have the option to build only the AWS KMS SDK. +Add the `-DBUILD_ONLY="kms"` flag and `-DBUILD_SHARED_LIBS=ON|OFF` to `cmake` in the instructions provided. - sudo apt-get update - sudo apt-get install -y libssl-dev cmake gcc +[Follow the AWS SDK for C++ build instructions](https://docs.aws.amazon.com/sdk-for-cpp/v1/developer-guide/setup-linux.html). -Now build and install aws-c-common: +Now, build and install the AWS Encryption SDK for C: - git clone /~https://github.com/awslabs/aws-c-common.git - mkdir build-aws-c-common && cd build-aws-c-common - cmake -DBUILD_SHARED_LIBS=ON ../aws-c-common - make && sudo make install ; cd .. - -#### Ubuntu: Build and install the AWS Encryption SDK for C - - git clone /~https://github.com/aws/aws-encryption-sdk-c.git + git clone --recurse-submodules /~https://github.com/aws/aws-encryption-sdk-c.git mkdir build-aws-encryption-sdk-c && cd build-aws-encryption-sdk-c - cmake -DBUILD_SHARED_LIBS=ON ../aws-encryption-sdk-c + cmake ../aws-encryption-sdk-c -DBUILD_SHARED_LIBS=ON make && sudo make install ; cd .. -You have successfully built and installed the AWS Encryption SDK for C. +### MacOS Build Recipe -### Building on Mac +[Homebrew](https://brew.sh) is a convenient way to get build tools for MacOS systems. -We recommend setting up [Homebrew](https://brew.sh/) to install some build tools. -Once it is set up, run the following: +With Homebrew installed, run the following: brew install openssl@1.1 cmake -(Note: Installing the AWS SDK for C++ through Homebrew does a full build, which -takes much longer than the KMS-only build. For these reasons, we recommend doing a source -build of the AWS SDK for C++ yourself, as we will demonstrate below.) - -Start in the directory where you want to do your build. - -#### Mac: (Option 1) C and C++ build dependencies - -Both aws-sdk-cpp and aws-c-common are required, but the installation of aws-sdk-cpp will install -aws-c-common for you. +The AWS SDK for C++ can be installed with Homebrew, which will install the full AWS SDK. If you +need the AWS SDK for C++ only to use the AWS Encryption SDK, you can build only the AWS KMS SDK. +See [these directions](https://docs.aws.amazon.com/sdk-for-cpp/v1/developer-guide/setup-linux.html#setup-linux-from-source) +and specify the `-DBUILD_ONLY="kms"` flag to `cmake` in the instructions provided. -Do a KMS-only build of the AWS SDK for C++. If you want to use the AWS SDK for C++ for -other AWS services, you can omit the `-DBUILD_ONLY="kms"` argument, but the build will take much longer. +Now, build and install the AWS Encryption SDK for C: - git clone -b 1.8.32 /~https://github.com/aws/aws-sdk-cpp.git - mkdir build-aws-sdk-cpp && cd build-aws-sdk-cpp - cmake -G Xcode -DBUILD_SHARED_LIBS=ON -DBUILD_ONLY="kms" -DENABLE_UNITY_BUILD=ON ../aws-sdk-cpp - xcodebuild -target install ; cd .. - -Now skip to the "Mac: Build and install the AWS Encryption SDK for C" section below. - -#### Mac: (Option 2) C only build dependencies - -Build and install aws-c-common: - - git clone -b v0.4.42 /~https://github.com/awslabs/aws-c-common.git - mkdir build-aws-c-common && cd build-aws-c-common - cmake -G Xcode -DBUILD_SHARED_LIBS=ON ../aws-c-common - xcodebuild -target install ; cd .. - -#### Mac: Build and install the AWS Encryption SDK for C - -Brew installed OpenSSL 1.1 to a place that is not picked up by default so we will -set the directory manually in our build. - - git clone /~https://github.com/aws/aws-encryption-sdk-c.git + git clone --recurse-submodules /~https://github.com/aws/aws-encryption-sdk-c.git mkdir build-aws-encryption-sdk-c && cd build-aws-encryption-sdk-c cmake -G Xcode -DBUILD_SHARED_LIBS=ON -DOPENSSL_ROOT_DIR="/usr/local/opt/openssl@1.1" ../aws-encryption-sdk-c xcodebuild -target install; cd .. -You have successfully built and installed the AWS Encryption SDK for C. - -### Building on Windows +### Windows Build Recipe -**Note**: _see the docker-images folder for some Windows build recipes that automate many of theses steps_ +**Note**: See the [docker-images folder](/~https://github.com/aws/aws-encryption-sdk-c/tree/master/docker-images) for some Windows build recipes that automate many of these steps. -Start by installing Visual Studio version 15 or later with the Windows Universal C Runtime and -[Git for Windows](https://git-scm.com/download/win). +**Note**: These instructions do not yet correctly build a statically-linked AWS Encryption SDK for C on Windows systems, i.e. with `-DBUILD_SHARED_LIBS=OFF`. We will update this README with instructions for that configuration soon. +Install Visual Studio version 15 or later with the Windows Universal C Runtime and [Git for Windows](https://git-scm.com/download/win). -Use the **x64 Native Tools Command Prompt** for all commands listed here. Run the following commands in the -directory where you want to do the build and installation. +Use the "x64 Native Tools Command Prompt" for all commands listed here. Run the following commands in the directory where you want to do the build and installation. - mkdir install && mkdir build && cd build - git clone /~https://github.com/Microsoft/vcpkg.git - cd vcpkg && .\bootstrap-vcpkg.bat - .\vcpkg install curl:x64-windows openssl:x64-windows && cd .. +Install Microsoft vcpkg by [following these directions](/~https://github.com/microsoft/vcpkg#quick-start-windows). Note the path to your `vcpkg.cmake` tool. This path will be something like `vcpkg\scripts\buildsystems\vcpkg.cmake` and you will need to pass it as `-DCMAKE_TOOLCHAIN_FILE` in your builds. -#### Windows: (Option 1) C and C++ build dependencies +Use vcpkg to install prerequisites: -Both aws-sdk-cpp and aws-c-common are required, but the installation of aws-sdk-cpp will install -aws-c-common for you. + vcpkg install curl:x64-windows openssl:x64-windows -Do a KMS-only build of the AWS SDK for C++. If you want to use the AWS SDK for C++ for -other AWS services, you can omit the `-DBUILD_ONLY="kms"` argument, but the build will take much longer. +You may also want to [configure vcpkg for Visual Studio CMake projects](/~https://github.com/microsoft/vcpkg#vcpkg-with-visual-studio-cmake-projects). - git clone /~https://github.com/aws/aws-sdk-cpp.git - mkdir build-aws-sdk-cpp && cd build-aws-sdk-cpp - cmake -DCMAKE_INSTALL_PREFIX=%cd%\..\..\install -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=ON -DENABLE_UNITY_BUILD=ON -DBUILD_ONLY=kms -DCMAKE_TOOLCHAIN_FILE=%cd%\..\vcpkg\scripts\buildsystems\vcpkg.cmake -G Ninja ..\aws-sdk-cpp - cmake --build . && cmake --build . --target install && cd .. +Build the AWS SDK for C++. This installs the aws-c-common dependency, too. If you need the AWS SDK for C++ only to use the +AWS Encryption SDK, you have the option to build only the AWS KMS SDK. Add the `-DBUILD_ONLY=kms` to build only the AWS KMS client. -Now continue to "Windows: Build and install the AWS Encryption SDK for C" below. +Follow [these instructions](https://docs.aws.amazon.com/sdk-for-cpp/v1/developer-guide/setup-windows.html#setup-windows-from-source), using `-DCMAKE_TOOLCHAIN_FILE` as described in the vcpkg setup instructions. Add `-DBUILD_SHARED_LIBS=ON` for shared libraries or `-DBUILD_SHARED_LIBS=OFF` for static libraries. -#### Windows: (Option 2) C only build dependency +Now, build and install the AWS Encryption SDK for C. Be sure to update `-DCMAKE_TOOLCHAIN_FILE` in the commands below. -Build and install aws-c-common: +Update `-DCMAKE_PREFIX_PATH` to the location of your AWS SDK for C++ and aws-c-common installations. - git clone /~https://github.com/awslabs/aws-c-common.git - mkdir build-aws-c-common && cd build-aws-c-common - cmake -DCMAKE_INSTALL_PREFIX=%cd%\..\..\install -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=ON -DCMAKE_TOOLCHAIN_FILE=%cd%\..\vcpkg\scripts\buildsystems\vcpkg.cmake -G Ninja ..\aws-c-common + git clone --recurse-submodules /~https://github.com/aws/aws-encryption-sdk-c.git + mkdir build-aws-encryption-sdk-c && cd build-aws-encryption-sdk-c + cmake -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=ON -DCMAKE_TOOLCHAIN_FILE"=%cd%\..\vcpkg\scripts\buildsystems\vcpkg.cmake" -DCMAKE_PREFIX_PATH="C:/Program Files (x86)/aws-cpp-sdk-all;C:/Program Files (x86)/aws-cpp-sdk-all/lib/aws-c-common" ..\aws-encryption-sdk-c cmake --build . && cmake --build . --target install && cd .. -#### Windows: Build and install the AWS Encryption SDK for C +## Building C only, without AWS KMS support - git clone /~https://github.com/aws/aws-encryption-sdk-c.git - mkdir build-aws-encryption-sdk-c && cd build-aws-encryption-sdk-c - cmake -DCMAKE_INSTALL_PREFIX=%cd%\..\..\install -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=ON -DCMAKE_TOOLCHAIN_FILE=%cd%\..\vcpkg\scripts\buildsystems\vcpkg.cmake -G Ninja ..\aws-encryption-sdk-c - cmake --build . && cmake --build . --target install && cd .. +If you don't need AWS KMS support, you can build the AWS Encryption SDK for C without the AWS SDK. This build is C-only with no C++ support +required. -You have successfully built and installed the AWS Encryption SDK for C. +To build without AWS KMS support, follow the build instructions above for your platform, substituting aws-c-common for aws-sdk-cpp. ## Doxygen Documentation @@ -265,10 +144,10 @@ Finally, run either `make doc_doxygen` (Unix), `MSBuild.exe .\doc_doxygen.vcxpro Once you have installed the AWS Encryption SDK for C, you are ready to start writing your own programs with it. -When doing a C compilation (not using the KMS keyring) be sure to include the flags +When doing a C compilation (not using the AWS KMS keyring) be sure to include the flags ``-lcrypto -laws-encryption-sdk -laws-c-common``. -When doing a C++ compilation (using the KMS keyring) be sure to include the flags +When doing a C++ compilation (using the AWS KMS keyring) be sure to include the flags ``-std=c++11 -lcrypto -laws-encryption-sdk -laws-encryption-sdk-cpp -laws-c-common -laws-cpp-sdk-kms -laws-cpp-sdk-core``. In the examples directory of this repo are several self-standing C and C++ files. @@ -284,7 +163,7 @@ knows how to find them. g++ -o string string.cpp -std=c++11 -lcrypto -laws-encryption-sdk -laws-encryption-sdk-cpp -laws-c-common -laws-cpp-sdk-kms -laws-cpp-sdk-core gcc -o raw_aes_keyring raw_aes_keyring.c -lcrypto -laws-encryption-sdk -laws-c-common -Note that the C++ files using the KMS keyring will require +Note that the C++ files using the AWS KMS keyring will require you to make sure that AWS credentials are set up on your machine to run properly. ## Tips and tricks @@ -311,7 +190,7 @@ the build use a particular installation of OpenSSL. By default the cmake for this project detects whether you have aws-sdk-cpp-core and aws-sdk-cpp-kms installed in a place it can find, and only if so will it build -the C++ components, (enabling use of the KMS keyring.) You can override the detection +the C++ components, (enabling use of the AWS KMS keyring.) You can override the detection logic by setting `-DBUILD_AWS_ENC_SDK_CPP=OFF` to never build the C++ components or by setting `-DBUILD_AWS_ENC_SDK_CPP=ON` to require building the C++ components (and fail if the C++ dependencies are not found.) diff --git a/SUPPORT_POLICY.rst b/SUPPORT_POLICY.rst new file mode 100644 index 000000000..0cb7b97a7 --- /dev/null +++ b/SUPPORT_POLICY.rst @@ -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 diff --git a/aws-encryption-sdk-cpp/tests/unit/t_cpputils.cpp b/aws-encryption-sdk-cpp/tests/unit/t_cpputils.cpp index 1c0bb10be..55c8d5337 100644 --- a/aws-encryption-sdk-cpp/tests/unit/t_cpputils.cpp +++ b/aws-encryption-sdk-cpp/tests/unit/t_cpputils.cpp @@ -24,22 +24,6 @@ using namespace Aws::Cryptosdk::Testing; const char *TEST_STRING = "Hello World!"; -static void *s_bad_malloc(struct aws_allocator *allocator, size_t size) { - return NULL; -} - -static void s_bad_free(struct aws_allocator *allocator, void *ptr) {} - -static void *s_bad_realloc(struct aws_allocator *allocator, void *ptr, size_t oldsize, size_t newsize) { - return NULL; -} - -static struct aws_allocator default_bad_allocator = { s_bad_malloc, s_bad_free, s_bad_realloc }; - -struct aws_allocator *t_aws_bad_allocator() { - return &default_bad_allocator; -} - int awsStringFromCAwsByteBuf_validInputs_returnAwsString() { struct aws_byte_buf b = aws_byte_buf_from_c_str(TEST_STRING); Aws::String b_string = aws_string_from_c_aws_byte_buf(&b); @@ -143,16 +127,6 @@ int appendKeyToEdks_appendSingleElement_elementIsAppended() { return 0; } -int appendKeyToEdks_allocatorThatDoesNotAllocateMemory_returnsOomError() { - struct aws_allocator *oom_allocator = t_aws_bad_allocator(); - EdksTestData ed; - TEST_ASSERT_ERROR( - AWS_ERROR_OOM, - t_append_c_str_key_to_edks( - oom_allocator, &ed.edks.encrypted_data_keys, &ed.enc, ed.data_key_id, ed.key_provider)); - return 0; -} - int appendKeyToEdks_multipleElementsAppended_elementsAreAppended() { EdksTestData ed1; EdksTestData ed2("enc2", "dk2", "kp2"); @@ -234,7 +208,6 @@ int main() { RUN_TEST(awsStringFromCAwsByteBuf_validInputs_returnAwsString()); RUN_TEST(awsUtilsByteBufferFromCAwsByteBuf_validInputs_returnAwsUtils()); RUN_TEST(appendKeyToEdks_appendSingleElement_elementIsAppended()); - RUN_TEST(appendKeyToEdks_allocatorThatDoesNotAllocateMemory_returnsOomError()); RUN_TEST(appendKeyToEdks_multipleElementsAppended_elementsAreAppended()); RUN_TEST(awsStringFromCAwsString_validInputs_returnAwsString()); RUN_TEST(awsMapFromCAwsHashHable_hashMap_returnAwsMap()); diff --git a/cbmc-ci/ci-config.yaml b/cbmc-ci/ci-config.yaml new file mode 100644 index 000000000..8d50f1655 --- /dev/null +++ b/cbmc-ci/ci-config.yaml @@ -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 diff --git a/switch-private-submodules b/switch-private-submodules new file mode 100755 index 000000000..d9c6ddfa8 --- /dev/null +++ b/switch-private-submodules @@ -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() diff --git a/verification/cbmc/.gitignore b/verification/cbmc/.gitignore index b29add68c..c44ec8e31 100644 --- a/verification/cbmc/.gitignore +++ b/verification/cbmc/.gitignore @@ -3,6 +3,7 @@ proofs/**/logs proofs/**/gotos proofs/**/report proofs/**/html +proofs/output # Emitted by CBMC Viewer TAGS-* diff --git a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-batch.yaml b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-batch.yaml deleted file mode 100644 index 4666fe0db..000000000 --- a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-batch.yaml +++ /dev/null @@ -1,17 +0,0 @@ -# Copyright 2018 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. - -jobos: ubuntu16 -cbmcflags: "--bounds-check;--pointer-check;--function;aws_cryptosdk_hdr_clean_up_verify;--unwindset;__builtin___memcpy_chk.0:4,memcpy_chk.0:4,memcpy.0:4,aws_cryptosdk_hdr_clean_up.0:2,aws_cryptosdk_hdr_clean_up.1:2,get_aws_cryptosdk_hdr_ptr.0:2,get_aws_cryptosdk_hdr_ptr.1:2;--unwinding-assertions;--trace;--memory-leak-check" -goto: proofs.goto -expected: "SUCCESSFUL" diff --git a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-proof.txt b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-batch.yaml b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-batch.yaml deleted file mode 100644 index 17fb85881..000000000 --- a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-batch.yaml +++ /dev/null @@ -1,17 +0,0 @@ -# Copyright 2018 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. - -jobos: ubuntu16 -cbmcflags: "--bounds-check;--pointer-check;--function;aws_cryptosdk_hdr_size_verify;--unwindset;aws_cryptosdk_hdr_size.0:2,aws_cryptosdk_hdr_size.1:2,get_aws_cryptosdk_hdr_ptr.0:2,get_aws_cryptosdk_hdr_ptr.1:2;--pointer-check;--trace;--unwinding-assertions" -goto: proofs.goto -expected: "SUCCESSFUL" diff --git a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-proof.txt b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-batch.yaml b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-batch.yaml deleted file mode 100644 index dac0823ec..000000000 --- a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-batch.yaml +++ /dev/null @@ -1,17 +0,0 @@ -# Copyright 2018 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. - -jobos: ubuntu16 -cbmcflags: "--bounds-check;--pointer-check;--function;aws_cryptosdk_hdr_write_verify;--unwindset;__builtin___memcpy_chk.0:5,memcpy_chk.0:5,memcpy.0:5,aws_cryptosdk_hdr_clean_up.0:0,aws_cryptosdk_hdr_clean_up.1:0,aws_mem_release:0,__builtin__memset_chk.0:2,memset.0:2,aws_cryptosdk_hdr_write.0:4,aws_cryptosdk_hdr_write.1:2,aws_cryptosdk_hdr_write.2:2,get_aws_cryptosdk_hdr_ptr.0:2,get_aws_cryptosdk_hdr_ptr.1:2;--pointer-check;--trace;--unwinding-assertions" -goto: proofs.goto -expected: "SUCCESSFUL" diff --git a/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-proof.txt b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-batch.yaml b/verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-batch.yaml deleted file mode 100644 index da39ac82c..000000000 --- a/verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-batch.yaml +++ /dev/null @@ -1,17 +0,0 @@ -# Copyright 2018 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. - -jobos: ubuntu16 -cbmcflags: "--bounds-check;--pointer-check;--function;hdr_zeroize_verify" -goto: proofs.goto -expected: "SUCCESSFUL" diff --git a/verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-proof.txt b/verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml deleted file mode 100644 index d06a00688..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;flush_openssl_errors.0:1;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_aes_gcm_decrypt_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-batch.yaml deleted file mode 100644 index edf19c501..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;flush_openssl_errors.0:1;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_aes_gcm_encrypt_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-batch.yaml deleted file mode 100644 index c1592500c..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_alg_props_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_alg_props/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-batch.yaml deleted file mode 100644 index ae6402076..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_cmm_base_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-batch.yaml deleted file mode 100644 index 2a56f1211..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_cmm_decrypt_materials_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-batch.yaml deleted file mode 100644 index 0dfb4c18a..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_cmm_generate_enc_materials_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/cbmc-batch.yaml deleted file mode 100644 index d901745a3..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_cmm_release_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/cbmc-batch.yaml deleted file mode 100644 index 674f61ec7..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_cmm_retain_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-batch.yaml deleted file mode 100644 index 92bb4f4cd..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;memcmp.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_compare_hash_elems_by_key_string_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/cbmc-batch.yaml deleted file mode 100644 index 15d331f4f..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_trace_has_allocated_records.0:2,aws_cryptosdk_keyring_trace_clear.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_dec_materials_destroy_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/cbmc-batch.yaml deleted file mode 100644 index 51e1153a8..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:11;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_dec_materials_new_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/cbmc-batch.yaml deleted file mode 100644 index b7e2f0221..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_decrypt_body.0:5,strlen.0:37;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_decrypt_body_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/cbmc-batch.yaml deleted file mode 100644 index 08355d6bf..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/cbmc-batch.yaml +++ /dev/null @@ -1,5 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. - \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/cbmc-batch.yaml deleted file mode 100644 index 9dcbe42ba..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_deserialize_frame_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/cbmc-batch.yaml deleted file mode 100644 index 18599c86b..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_clean_up_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/cbmc-batch.yaml deleted file mode 100644 index deff91d57..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_eq_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/cbmc-batch.yaml deleted file mode 100644 index e25055b92..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_init_clone_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/cbmc-batch.yaml deleted file mode 100644 index 4c598a13e..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:3,aws_cryptosdk_edk_list_elements_are_bounded.0:3,aws_cryptosdk_edk_list_elements_are_valid.0:3,aws_cryptosdk_edk_list_is_bounded.0:3,aws_cryptosdk_edk_list_is_valid.0:3,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:3,ensure_cryptosdk_edk_list_has_allocated_members.0:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_list_clean_up_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/cbmc-batch.yaml deleted file mode 100644 index 2948f1517..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:3,aws_cryptosdk_edk_list_elements_are_bounded.0:3,aws_cryptosdk_edk_list_elements_are_valid.0:3,aws_cryptosdk_edk_list_is_bounded.0:3,aws_cryptosdk_edk_list_is_valid.0:3,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:3,ensure_cryptosdk_edk_list_has_allocated_members.0:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_list_clear_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/cbmc-batch.yaml deleted file mode 100644 index de09afe36..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;__CPROVER_file_local_list_utils_c_list_copy_all.5:3,__CPROVER_file_local_list_utils_c_list_copy_all.6:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_list_copy_all_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/cbmc-batch.yaml deleted file mode 100644 index c380c1316..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_edk_list_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/cbmc-batch.yaml deleted file mode 100644 index 33130b392..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_hash_table_clear.0:5,memset_override_0_impl.0:23;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_clean_up_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/cbmc-batch.yaml deleted file mode 100644 index c96879a8a..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_hash_table_clear.0:5,memset_override_0_impl.0:23;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_clear_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/cbmc-batch.yaml deleted file mode 100644 index a244056bb..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_enc_ctx_clone.0:5,aws_cryptosdk_enc_ctx_clone.1:5;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_clone_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/cbmc-batch.yaml deleted file mode 100644 index 2c8add330..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_enc_ctx_deserialize.0:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_deserialize_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/cbmc-batch.yaml deleted file mode 100644 index 58075b510..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/cbmc-batch.yaml deleted file mode 100644 index 977e4e072..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;array_list_item_generator.0:3,aws_cryptosdk_enc_ctx_serialize.0:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_serialize_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile index 9314ca54b..8c5bc5e23 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile @@ -58,4 +58,6 @@ UNWINDSET += aws_cryptosdk_enc_ctx_size.0:$(call addone,$(MAX_TABLE_SIZE)) UNWINDSET += memset_override_0_impl.0:$(call addone,$(TABLE_SIZE_IN_WORDS)) ########### +EXPENSIVE = true + include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/cbmc-batch.yaml deleted file mode 100644 index 44bbe5765..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_add_size_checked_varargs.0:5,aws_cryptosdk_enc_ctx_size.0:17,memset_override_0_impl.0:59;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_ctx_size_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/cbmc-batch.yaml deleted file mode 100644 index d7ac59323..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_materials_destroy_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/cbmc-batch.yaml deleted file mode 100644 index b9565e957..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:11;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_enc_materials_new_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/cbmc-batch.yaml deleted file mode 100644 index dcf4c04cc..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_encrypt_body.0:5,strlen.0:37;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_encrypt_body_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_genrandom/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_genrandom/cbmc-batch.yaml deleted file mode 100644 index b020883ed..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_genrandom/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_genrandom_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_genrandom/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_genrandom/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_genrandom/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/cbmc-batch.yaml deleted file mode 100644 index c05fa8881..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_hash_elems_array_init.0:5;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_hash_elems_array_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_size/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_hdr_size/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_hdr_size/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_size/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_hdr_size/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_hdr_size/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_hkdf/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_hkdf/cbmc-batch.yaml deleted file mode 100644 index 694b05670..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_hkdf/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_hkdf_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_hkdf/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_hkdf/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_hkdf/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/cbmc-batch.yaml deleted file mode 100644 index 6f838fe78..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_base_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/cbmc-batch.yaml deleted file mode 100644 index 147eaa35e..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;memcmp.0:33,aws_cryptosdk_keyring_trace_is_valid.0:3,ensure_trace_has_allocated_records.0:3,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_on_decrypt_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/cbmc-batch.yaml deleted file mode 100644 index 26eedd11d..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;memcmp.0:33,aws_cryptosdk_keyring_trace_is_valid.0:3,ensure_trace_has_allocated_records.0:3,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_on_encrypt_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_release/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_release/cbmc-batch.yaml deleted file mode 100644 index 4986b3788..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_release/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_release_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_release/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_release/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_release/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/cbmc-batch.yaml deleted file mode 100644 index 27dac41d0..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_retain_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/cbmc-batch.yaml deleted file mode 100644 index 56621bf49..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:4,ensure_trace_has_allocated_records.0:3,aws_string_new_from_array.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_add_record_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/cbmc-batch.yaml deleted file mode 100644 index 4cdc920ef..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:4,ensure_trace_has_allocated_records.0:3,aws_string_new_from_array.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_add_record_buf_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/cbmc-batch.yaml deleted file mode 100644 index 20bdc118d..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:4,ensure_trace_has_allocated_records.0:3,aws_string_new_from_array.0:17,strlen.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_add_record_c_str_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/cbmc-batch.yaml deleted file mode 100644 index 7b76c5b94..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:3,ensure_trace_has_allocated_records.0:3,aws_cryptosdk_keyring_trace_clear.0:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_clean_up_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/cbmc-batch.yaml deleted file mode 100644 index 3e66ebcd1..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:3,ensure_trace_has_allocated_records.0:3,aws_cryptosdk_keyring_trace_clear.0:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_clear_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile index abdcaa3a4..bb9f6e03f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile @@ -64,5 +64,7 @@ UNWINDSET += __CPROVER_file_local_list_utils_c_list_copy_all.5:$(call addone,$(N UNWINDSET += __CPROVER_file_local_list_utils_c_list_copy_all.6:$(call addone,$(NUM_ELEMS)) UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(call addone,$(NUM_ELEMS)) +EXPENSIVE = true + ########### include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile index 842be09b3..411b750f7 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile @@ -43,4 +43,6 @@ UNWINDSET += ensure_trace_has_allocated_records.0:$(call addone,$(MAX_ITEM_SIZE) UNWINDSET += memcmp.0:$(call addone,$(MAX_STRING_LEN)) ########### +EXPENSIVE = true + include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/cbmc-batch.yaml deleted file mode 100644 index fabc9141b..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:3,ensure_trace_has_allocated_records.0:3,aws_cryptosdk_keyring_trace_eq.0:3,memcmp.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_eq_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/cbmc-batch.yaml deleted file mode 100644 index 12ccefc26..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/cbmc-batch.yaml deleted file mode 100644 index 944fc742f..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_record_clean_up_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/cbmc-batch.yaml deleted file mode 100644 index 29883d6b1..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;memcmp.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_keyring_trace_record_init_clone_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_abort/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_md_abort/cbmc-batch.yaml deleted file mode 100644 index 4ac5c8940..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_md_abort/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_md_abort_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_abort/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_md_abort/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_md_abort/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_finish/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_md_finish/cbmc-batch.yaml deleted file mode 100644 index 9f4c64b16..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_md_finish/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_md_finish_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_finish/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_md_finish/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_md_finish/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_init/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_md_init/cbmc-batch.yaml deleted file mode 100644 index 8f16fc10d..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_md_init/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_md_init_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_init/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_md_init/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_md_init/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_size/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_md_size/cbmc-batch.yaml deleted file mode 100644 index 2ce960814..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_md_size/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_md_size_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_size/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_md_size/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_md_size/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_update/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_md_update/cbmc-batch.yaml deleted file mode 100644 index 940161c72..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_md_update/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_md_update_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_update/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_md_update/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_md_update/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/cbmc-batch.yaml deleted file mode 100644 index dc64b32aa..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_multi_keyring_add_child_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/cbmc-batch.yaml deleted file mode 100644 index b3fb9d730..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: MultiKeyringNew_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index e0ecbedf5..84c8eab68 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -115,5 +115,7 @@ UNWINDSET += ensure_cryptosdk_edk_list_has_allocated_list_elements.0:$(call addo UNWINDSET += ensure_trace_has_allocated_records.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) UNWINDSET += memcmp.0:$(call addone,$(MAX_BUFFER_SIZE)) +EXPENSIVE = true + ########### include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/cbmc-batch.yaml deleted file mode 100644 index 27c5e1f91..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/cbmc-batch.yaml deleted file mode 100644 index ea28f1726..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_rsa_decrypt_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/cbmc-batch.yaml deleted file mode 100644 index 339c5f41c..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_rsa_encrypt_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/cbmc-batch.yaml deleted file mode 100644 index c900d1246..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_serialize_frame_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/cbmc-batch.yaml deleted file mode 100644 index ae333e8d6..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_abort_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/cbmc-batch.yaml deleted file mode 100644 index c527ca787..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_get_privkey_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/cbmc-batch.yaml deleted file mode 100644 index 9487648c8..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_base64_encode.0:22;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_get_pubkey_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/cbmc-batch.yaml deleted file mode 100644 index 9bdd101ab..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_sig_sign_finish.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_sign_finish_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/cbmc-batch.yaml deleted file mode 100644 index 4aa0e5649..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;strcmp.0:11;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_sign_start_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/cbmc-batch.yaml deleted file mode 100644 index be54903b9..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;strcmp.0:11;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_sign_start_keygen_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_update/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_update/cbmc-batch.yaml deleted file mode 100644 index 8d1509c55..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_update/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--memory-leak-check;--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_update_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_update/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_update/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_update/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/cbmc-batch.yaml deleted file mode 100644 index 7f835a0d2..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_verify_finish_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/cbmc-batch.yaml deleted file mode 100644 index c4d039217..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;strcmp.0:11;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sig_verify_start_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_sign_header/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_sign_header/cbmc-batch.yaml deleted file mode 100644 index cfc774e24..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_sign_header/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_sign_header_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_sign_header/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_sign_header/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_sign_header/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_string_dup/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_string_dup/cbmc-batch.yaml deleted file mode 100644 index 40571b19f..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_string_dup/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;memcmp.0:17;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_string_dup_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_string_dup/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_string_dup/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_string_dup/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/cbmc-batch.yaml deleted file mode 100644 index 541bc1803..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_transfer_list.4:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_transfer_list_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/aws_cryptosdk_verify_header/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_verify_header/cbmc-batch.yaml deleted file mode 100644 index bebfb820d..000000000 --- a/verification/cbmc/proofs/aws_cryptosdk_verify_header/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;__CPROVER_file_local_cipher_c_flush_openssl_errors.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_verify_header_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/aws_cryptosdk_verify_header/cbmc-proof.txt b/verification/cbmc/proofs/aws_cryptosdk_verify_header/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_verify_header/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-batch.yaml b/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-proof.txt b/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/derive_data_key/cbmc-batch.yaml b/verification/cbmc/proofs/derive_data_key/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/derive_data_key/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/derive_data_key/cbmc-proof.txt b/verification/cbmc/proofs/derive_data_key/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/derive_data_key/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/list_copy_all/cbmc-batch.yaml b/verification/cbmc/proofs/list_copy_all/cbmc-batch.yaml deleted file mode 100644 index 24cb521ee..000000000 --- a/verification/cbmc/proofs/list_copy_all/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;__CPROVER_file_local_list_utils_c_list_copy_all.5:3,__CPROVER_file_local_list_utils_c_list_copy_all.6:3;--object-bits;8" -expected: "SUCCESSFUL" -goto: list_copy_all_harness.goto -jobos: ubuntu16 diff --git a/verification/cbmc/proofs/list_copy_all/cbmc-proof.txt b/verification/cbmc/proofs/list_copy_all/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/list_copy_all/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/proofs/run-cbmc-proofs.py b/verification/cbmc/proofs/run-cbmc-proofs.py deleted file mode 100755 index 2d2ed272c..000000000 --- a/verification/cbmc/proofs/run-cbmc-proofs.py +++ /dev/null @@ -1,258 +0,0 @@ -#!/usr/bin/env python3 -# -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - - -import argparse -import asyncio -import logging -import math -import os -import pathlib -import subprocess -import sys - - -DESCRIPTION = "Configure and run all CBMC proofs in parallel" - -# Keep the epilog hard-wrapped at 70 characters, as it gets printed -# verbatim in the terminal. 70 characters stops here --------------> | -EPILOG = """ -This tool automates the process of running `make report` in each of -the CBMC proof directories. The tool calculates the dependency graph -of all tasks needed to build, run, and report on all the proofs, and -executes these tasks in parallel. - -The tool is roughly equivalent to doing this: - - litani init --project "my-cool-project"; - - find . -name cbmc-batch.yaml | while read -r proof; do - pushd $(dirname ${proof}); - - # The `make _report` rule adds a single proof to litani - # without running it - make _report; - - popd; - done - - litani run-build; - -except that it is much faster and provides some convenience options. -The CBMC CI runs this script with no arguments to build and run all -proofs in parallel. The value of "my-cool-project" is taken from the -PROJECT_NAME variable in Makefile-project-defines. - -The --no-standalone argument omits the `litani init` and `litani -run-build`; use it when you want to add additional proof jobs, not -just the CBMC ones. In that case, you would run `litani init` -yourself; then run `run-cbmc-proofs --no-standalone`; add any -additional jobs that you want to execute with `litani add-job`; and -finally run `litani run-build`. -""" - - -def get_project_name(): - cmd = [ - "make", - "-f", "Makefile.common", - "echo-project-name", - ] - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) - if proc.returncode: - logging.critical("could not run make to determine project name") - sys.exit(1) - if not proc.stdout.strip(): - logging.warning( - "project name has not been set; using generic name instead. " - "Set the PROJECT_NAME value in Makefile-project-defines to " - "remove this warning") - return "" - return proc.stdout.strip() - - -def get_args(): - pars = argparse.ArgumentParser( - description=DESCRIPTION, epilog=EPILOG, - formatter_class=argparse.RawDescriptionHelpFormatter) - for arg in [{ - "flags": ["-j", "--parallel-jobs"], - "type": int, - "metavar": "N", - "help": "run at most N proof jobs in parallel", - }, { - "flags": ["--no-standalone"], - "action": "store_true", - "help": "only configure proofs: do not initialize nor run", - }, { - "flags": ["-p", "--proofs"], - "nargs": "+", - "metavar": "DIR", - "help": "only run proof in directory DIR (can pass more than one)", - }, { - "flags": ["--project-name"], - "metavar": "NAME", - "default": get_project_name(), - "help": "project name for report. Default: %(default)s", - }, { - "flags": ["--proof-marker"], - "metavar": "FILE", - "default": "cbmc-batch.yaml", - "help": ( - "name of file that marks proof directories. Default: " - "%(default)s"), - }, { - "flags": ["--verbose"], - "action": "store_true", - "help": "verbose output", - }]: - flags = arg.pop("flags") - pars.add_argument(*flags, **arg) - return pars.parse_args() - - -def set_up_logging(verbose): - if verbose: - level = logging.DEBUG - else: - level = logging.WARNING - logging.basicConfig( - format="run-cbmc-proofs: %(message)s", level=level) - - -def task_pool_size(): - ret = os.cpu_count() - if ret is None or ret < 3: - return 1 - return ret - 2 - - -def print_counter(counter): - print( - "\rConfiguring CBMC proofs: " - "{complete:{width}} / {total:{width}}".format( - **counter), end="", file=sys.stderr) - - -def get_proof_dirs(proof_root, proof_list, proof_marker): - if proof_list is not None: - proofs_remaining = list(proof_list) - else: - proofs_remaining = [] - - for root, _, fyles in os.walk(proof_root): - proof_name = str(pathlib.Path(root).name) - if proof_list and proof_name not in proof_list: - continue - if proof_list and proof_name in proofs_remaining: - proofs_remaining.remove(proof_name) - if proof_marker in fyles: - yield root - - if proofs_remaining: - logging.critical( - "The following proofs were not found: %s", - ", ".join(proofs_remaining)) - sys.exit(1) - - -def run_build(litani, jobs): - cmd = [str(litani), "run-build"] - if jobs: - cmd.extend(["-j", str(jobs)]) - - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd) - if proc.returncode: - logging.critical("Failed to run litani run-build") - sys.exit(1) - - -def get_litani_path(proof_root): - cmd = [ - "make", - "PROOF_ROOT=%s" % proof_root, - "-f", "Makefile.common", - "litani-path", - ] - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) - if proc.returncode: - logging.critical("Could not determine path to litani") - sys.exit(1) - return proc.stdout.strip() - - -async def configure_proof_dirs(queue, counter): - while True: - print_counter(counter) - path = str(await queue.get()) - - proc = await asyncio.create_subprocess_exec( - "nice", "-n", "15", "make", "-B", "--quiet", "_report", cwd=path) - await proc.wait() - counter["fail" if proc.returncode else "pass"].append(path) - counter["complete"] += 1 - - print_counter(counter) - queue.task_done() - - -async def main(): - args = get_args() - set_up_logging(args.verbose) - - proof_root = pathlib.Path(__file__).resolve().parent - litani = get_litani_path(proof_root) - - if not args.no_standalone: - cmd = [str(litani), "init", "--project", args.project_name] - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd) - if proc.returncode: - logging.critical("Failed to run litani init") - sys.exit(1) - - proof_dirs = list(get_proof_dirs( - proof_root, args.proofs, args.proof_marker)) - if not proof_dirs: - logging.critical("No proof directories found") - sys.exit(1) - - proof_queue = asyncio.Queue() - for proof_dir in proof_dirs: - proof_queue.put_nowait(proof_dir) - - counter = { - "pass": [], - "fail": [], - "complete": 0, - "total": len(proof_dirs), - "width": int(math.log10(len(proof_dirs))) + 1 - } - - tasks = [] - for _ in range(task_pool_size()): - task = asyncio.create_task(configure_proof_dirs( - proof_queue, counter)) - tasks.append(task) - - await proof_queue.join() - - print_counter(counter) - print("", file=sys.stderr) - - if counter["fail"]: - logging.critical( - "Failed to configure the following proofs:\n%s", "\n".join( - [str(f) for f in counter["fail"]])) - - if not args.no_standalone: - run_build(litani, args.parallel_jobs) - - -if __name__ == "__main__": - asyncio.run(main()) diff --git a/verification/cbmc/proofs/run-cbmc-proofs.py b/verification/cbmc/proofs/run-cbmc-proofs.py new file mode 120000 index 000000000..76b1ad326 --- /dev/null +++ b/verification/cbmc/proofs/run-cbmc-proofs.py @@ -0,0 +1 @@ +../templates/template-for-repository/proofs/run-cbmc-proofs.py \ No newline at end of file diff --git a/verification/cbmc/proofs/sign_header/cbmc-batch.yaml b/verification/cbmc/proofs/sign_header/cbmc-batch.yaml deleted file mode 100644 index e936b4599..000000000 --- a/verification/cbmc/proofs/sign_header/cbmc-batch.yaml +++ /dev/null @@ -1,4 +0,0 @@ -: - This file marks this directory as containing a CBMC proof. This file - is automatically clobbered in CI and replaced with parameters for - running the proof. \ No newline at end of file diff --git a/verification/cbmc/proofs/sign_header/cbmc-proof.txt b/verification/cbmc/proofs/sign_header/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/sign_header/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof diff --git a/verification/cbmc/templates b/verification/cbmc/templates index 8f2dafc1d..7fdd7048b 160000 --- a/verification/cbmc/templates +++ b/verification/cbmc/templates @@ -1 +1 @@ -Subproject commit 8f2dafc1db539ca97b6f4b8533f069e176c11b1c +Subproject commit 7fdd7048b01e68fd549e20da1d216e34d719043a diff --git a/verification/litani b/verification/litani index b65229507..8b23cb74d 160000 --- a/verification/litani +++ b/verification/litani @@ -1 +1 @@ -Subproject commit b652295078e26f8444c72ee3088f6a1230624827 +Subproject commit 8b23cb74d5ca47e0f94ee50bb3da7e907fd48f27