Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Update proof tools (+disable submodule cloning by default) #20

Merged
merged 2 commits into from
Jul 20, 2021

Conversation

sukhmanm
Copy link
Contributor

@sukhmanm sukhmanm commented Jul 14, 2021

Description of changes: Advance CBMC pointers (see ex. FreeRTOS/coreHTTP#107), and update .gitmodules to disable default behavior of cloning submodules.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@sukhmanm sukhmanm marked this pull request as ready for review July 17, 2021 01:11
This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:

- Profiling
    - Litani measures the memory usage of the CBMC safety checking and
      coverage checking jobs
    - The dashboard includes box-and-whisker diagrams for memory use per
      proof
    - The dashboard includes a graph of how many parallel jobs are
      running over the whole run, making it easy to choose a CI machine
      with enough parallelism
    - It is now possible to designate particular proofs as "EXPENSIVE";
      Litani runs expensive proofs serially, ensuring that they do not
      over-consume resources like RAM.

- UI improvements
    - Each pipeline page includes a table of contents
    - Each pipeline page includes a dependency graph of the pipeline
    - Each job on the pipeline page has a hyperlink to that job
    - The terminal output is now less noisy
@sukhmanm sukhmanm changed the title [Draft/Test] Standard submodule pointer + disable cloning by default Update proof tools (+disable submodule cloning by default) Jul 17, 2021
@sukhmanm sukhmanm merged commit 2e4bd59 into aws:main Jul 20, 2021
@sukhmanm sukhmanm deleted the cbmc-test branch July 20, 2021 19:36
yourslab pushed a commit to yourslab/SigV4-for-AWS-IoT-embedded-sdk-1 that referenced this pull request Aug 6, 2021
Update auto-generated .md files

Add test and tool directories (aws#1)

Adding test and tools directories, with CMock submodule.

CI Actions (aws#2)

Add header files + default configurations (aws#3)

- Add files sigv4.h and sigv4_config_defaults.h
- Add public-facing API elements detailed in design doc

Format Date Header for ISO8601 Compliance (aws#4)

Add optional utility function to format date header returned from AWS IoT (ex. in temp tokens) for compliance with the ISO8601 format required for authentication

Add unit tests for SigV4_AwsIotDateToIso8601() (aws#8)

Setup proof infrastructure for CBMC (aws#7)

* Add Litani and templates for CBMC

* Add sample proof

* Implement CBMC proof for SigV4_AwsIotDateToIso8601

* Unwind all loops such that no unwinding errors occur

Change submodule to use https rather than ssh for aws-templates-for-cbmc-proofs (aws#12)

* CBMC fix test (do not merge)

* Change AWS templates to https instead of ssh

* Revert README

Update README.md and LICENSE files (aws#14)

Update README.md and LICENSE files before changing repo's visibility status (to public).

Add remaining doxygen + link verification checks (aws#15)

Add doxygen + link verifier checks (the library-specific doxygen content will be added in a separate PR for further review).

[SigV4] CBMC proof for Sigv4_awsIotdatetoISO8601 API (aws#19)

* Sigv4_AWSIOtDateToISO8601 CBMC PROOF

* Unit test coverage changes

Add release workflow (+ revert to previous license) (aws#18)

change permissions of run_cbmc_proofs.py (aws#21)

[Sigv4] Doxygen content updates (aws#22)

* doxygen doc update

* lexicon update

Update proof tools (+disable submodule cloning by default) (aws#20)

This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:

- Profiling
    - Litani measures the memory usage of the CBMC safety checking and
      coverage checking jobs
    - The dashboard includes box-and-whisker diagrams for memory use per
      proof
    - The dashboard includes a graph of how many parallel jobs are
      running over the whole run, making it easy to choose a CI machine
      with enough parallelism
    - It is now possible to designate particular proofs as "EXPENSIVE";
      Litani runs expensive proofs serially, ensuring that they do not
      over-consume resources like RAM.

- UI improvements
    - Each pipeline page includes a table of contents
    - Each pipeline page includes a dependency graph of the pipeline
    - Each job on the pipeline page has a hyperlink to that job
    - The terminal output is now less noisy

SigV4_GenerateHTTPAuthorization() API Functionality (aws#16)

* Squash of outdated aws#13 commits

* Hold for checks

* Add definitions for sorting structures

* Include parsing functions

* Fix old commit error

* Missing asserts

* (temporarily allow warnings)

* Spell check + include partial context

* More updates to lexicon+doxygen

* Add asserts for private func.

* Move access after asserts

* Clarify pointer increment

* Update postfix syntax for correct operator precedence

* Feedback changes only

* + remove accidental duplicate

Implement credential scope

Implement generate credential query

Validation of parameter count

Solution a bit overcomplicated

Squash bugs and canonical query parameters should also be sorted by value

Finish canonicalize query

Fix canonical URI encoding

Add hash helper function

Add hmac implementation

Add newline chars for canonical request

Finish writing of canonical request

Hex-encoded hash of canonical request matches

Write string to sign

Fix bug

Refactor writeStringToSign for complexity

Allow HMAC keys to be passed through separate function calls

Add code for generating signing key

Fix hmac bug

Generate the final signature correctly

Fix bug

Fix newline not being written

Merge Shivangi's code

Stylistic changes

Link OpenSSL to the test

Add unit tests attaining branch coverage of 71%

Integrate Shivangi's latest changes

Output authBufLen when complete

Update logic when headers are precanonicalized.

Add additional parameter checks for block/digest len

Add documentation

Fix test case

Get complexity <= 8 for private functions

Reduce complexity

Remove use of %zu

Revert changes to test as it was added to another PR

Uncrustify and add doxygen strings.

Add docs

Resolve doxygen errors and lexicon.txt

Document all private functions

Fix remaining doxygen errors

Update lexicon.txt

Remove duplicate declaration

Remove assertions on pQuery being NULL

Add log messages for insufficient memory errors

Uncrustify
yourslab pushed a commit to yourslab/SigV4-for-AWS-IoT-embedded-sdk-1 that referenced this pull request Aug 6, 2021
Update auto-generated .md files

Add test and tool directories (aws#1)

Adding test and tools directories, with CMock submodule.

CI Actions (aws#2)

Add header files + default configurations (aws#3)

- Add files sigv4.h and sigv4_config_defaults.h
- Add public-facing API elements detailed in design doc

Format Date Header for ISO8601 Compliance (aws#4)

Add optional utility function to format date header returned from AWS IoT (ex. in temp tokens) for compliance with the ISO8601 format required for authentication

Add unit tests for SigV4_AwsIotDateToIso8601() (aws#8)

Setup proof infrastructure for CBMC (aws#7)

* Add Litani and templates for CBMC

* Add sample proof

* Implement CBMC proof for SigV4_AwsIotDateToIso8601

* Unwind all loops such that no unwinding errors occur

Change submodule to use https rather than ssh for aws-templates-for-cbmc-proofs (aws#12)

* CBMC fix test (do not merge)

* Change AWS templates to https instead of ssh

* Revert README

Update README.md and LICENSE files (aws#14)

Update README.md and LICENSE files before changing repo's visibility status (to public).

Add remaining doxygen + link verification checks (aws#15)

Add doxygen + link verifier checks (the library-specific doxygen content will be added in a separate PR for further review).

[SigV4] CBMC proof for Sigv4_awsIotdatetoISO8601 API (aws#19)

* Sigv4_AWSIOtDateToISO8601 CBMC PROOF

* Unit test coverage changes

Add release workflow (+ revert to previous license) (aws#18)

change permissions of run_cbmc_proofs.py (aws#21)

[Sigv4] Doxygen content updates (aws#22)

* doxygen doc update

* lexicon update

Update proof tools (+disable submodule cloning by default) (aws#20)

This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:

- Profiling
    - Litani measures the memory usage of the CBMC safety checking and
      coverage checking jobs
    - The dashboard includes box-and-whisker diagrams for memory use per
      proof
    - The dashboard includes a graph of how many parallel jobs are
      running over the whole run, making it easy to choose a CI machine
      with enough parallelism
    - It is now possible to designate particular proofs as "EXPENSIVE";
      Litani runs expensive proofs serially, ensuring that they do not
      over-consume resources like RAM.

- UI improvements
    - Each pipeline page includes a table of contents
    - Each pipeline page includes a dependency graph of the pipeline
    - Each job on the pipeline page has a hyperlink to that job
    - The terminal output is now less noisy

SigV4_GenerateHTTPAuthorization() API Functionality (aws#16)

* Squash of outdated aws#13 commits

* Hold for checks

* Add definitions for sorting structures

* Include parsing functions

* Fix old commit error

* Missing asserts

* (temporarily allow warnings)

* Spell check + include partial context

* More updates to lexicon+doxygen

* Add asserts for private func.

* Move access after asserts

* Clarify pointer increment

* Update postfix syntax for correct operator precedence

* Feedback changes only

* + remove accidental duplicate

Implement credential scope

Implement generate credential query

Validation of parameter count

Solution a bit overcomplicated

Squash bugs and canonical query parameters should also be sorted by value

Finish canonicalize query

Fix canonical URI encoding

Add hash helper function

Add hmac implementation

Add newline chars for canonical request

Finish writing of canonical request

Hex-encoded hash of canonical request matches

Write string to sign

Fix bug

Refactor writeStringToSign for complexity

Allow HMAC keys to be passed through separate function calls

Add code for generating signing key

Fix hmac bug

Generate the final signature correctly

Fix bug

Fix newline not being written

Merge Shivangi's code

Stylistic changes

Link OpenSSL to the test

Add unit tests attaining branch coverage of 71%

Integrate Shivangi's latest changes

Output authBufLen when complete

Update logic when headers are precanonicalized.

Add additional parameter checks for block/digest len

Add documentation

Fix test case

Get complexity <= 8 for private functions

Reduce complexity

Remove use of %zu

Revert changes to test as it was added to another PR

Uncrustify and add doxygen strings.

Add docs

Resolve doxygen errors and lexicon.txt

Document all private functions

Fix remaining doxygen errors

Update lexicon.txt

Remove duplicate declaration

Remove assertions on pQuery being NULL

Add log messages for insufficient memory errors

Uncrustify
yourslab pushed a commit to yourslab/SigV4-for-AWS-IoT-embedded-sdk-1 that referenced this pull request Aug 9, 2021
Update auto-generated .md files

Add test and tool directories (aws#1)

Adding test and tools directories, with CMock submodule.

CI Actions (aws#2)

Add header files + default configurations (aws#3)

- Add files sigv4.h and sigv4_config_defaults.h
- Add public-facing API elements detailed in design doc

Format Date Header for ISO8601 Compliance (aws#4)

Add optional utility function to format date header returned from AWS IoT (ex. in temp tokens) for compliance with the ISO8601 format required for authentication

Add unit tests for SigV4_AwsIotDateToIso8601() (aws#8)

Setup proof infrastructure for CBMC (aws#7)

* Add Litani and templates for CBMC

* Add sample proof

* Implement CBMC proof for SigV4_AwsIotDateToIso8601

* Unwind all loops such that no unwinding errors occur

Change submodule to use https rather than ssh for aws-templates-for-cbmc-proofs (aws#12)

* CBMC fix test (do not merge)

* Change AWS templates to https instead of ssh

* Revert README

Update README.md and LICENSE files (aws#14)

Update README.md and LICENSE files before changing repo's visibility status (to public).

Add remaining doxygen + link verification checks (aws#15)

Add doxygen + link verifier checks (the library-specific doxygen content will be added in a separate PR for further review).

[SigV4] CBMC proof for Sigv4_awsIotdatetoISO8601 API (aws#19)

* Sigv4_AWSIOtDateToISO8601 CBMC PROOF

* Unit test coverage changes

Add release workflow (+ revert to previous license) (aws#18)

change permissions of run_cbmc_proofs.py (aws#21)

[Sigv4] Doxygen content updates (aws#22)

* doxygen doc update

* lexicon update

Update proof tools (+disable submodule cloning by default) (aws#20)

This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:

- Profiling
    - Litani measures the memory usage of the CBMC safety checking and
      coverage checking jobs
    - The dashboard includes box-and-whisker diagrams for memory use per
      proof
    - The dashboard includes a graph of how many parallel jobs are
      running over the whole run, making it easy to choose a CI machine
      with enough parallelism
    - It is now possible to designate particular proofs as "EXPENSIVE";
      Litani runs expensive proofs serially, ensuring that they do not
      over-consume resources like RAM.

- UI improvements
    - Each pipeline page includes a table of contents
    - Each pipeline page includes a dependency graph of the pipeline
    - Each job on the pipeline page has a hyperlink to that job
    - The terminal output is now less noisy

SigV4_GenerateHTTPAuthorization() API Functionality (aws#16)

* Squash of outdated aws#13 commits

* Hold for checks

* Add definitions for sorting structures

* Include parsing functions

* Fix old commit error

* Missing asserts

* (temporarily allow warnings)

* Spell check + include partial context

* More updates to lexicon+doxygen

* Add asserts for private func.

* Move access after asserts

* Clarify pointer increment

* Update postfix syntax for correct operator precedence

* Feedback changes only

* + remove accidental duplicate

Implement credential scope

Implement generate credential query

Validation of parameter count

Solution a bit overcomplicated

Squash bugs and canonical query parameters should also be sorted by value

Finish canonicalize query

Fix canonical URI encoding

Add hash helper function

Add hmac implementation

Add newline chars for canonical request

Finish writing of canonical request

Hex-encoded hash of canonical request matches

Write string to sign

Fix bug

Refactor writeStringToSign for complexity

Allow HMAC keys to be passed through separate function calls

Add code for generating signing key

Fix hmac bug

Generate the final signature correctly

Fix bug

Fix newline not being written

Merge Shivangi's code

Stylistic changes

Link OpenSSL to the test

Add unit tests attaining branch coverage of 71%

Integrate Shivangi's latest changes

Output authBufLen when complete

Update logic when headers are precanonicalized.

Add additional parameter checks for block/digest len

Add documentation

Fix test case

Get complexity <= 8 for private functions

Reduce complexity

Remove use of %zu

Revert changes to test as it was added to another PR

Uncrustify and add doxygen strings.

Add docs

Resolve doxygen errors and lexicon.txt

Document all private functions

Fix remaining doxygen errors

Update lexicon.txt

Remove duplicate declaration

Remove assertions on pQuery being NULL

Add log messages for insufficient memory errors

Uncrustify
yourslab added a commit that referenced this pull request Aug 15, 2021
* Link OpenSSL to the test

* Add unit tests attaining branch coverage of 71%

* Output authBufLen when complete

* Fix test case

* Revert changes to sigv4 sources

* SigV4_GenerateHTTPAuthorization Implementation

Update auto-generated .md files

Add test and tool directories (#1)

Adding test and tools directories, with CMock submodule.

CI Actions (#2)

Add header files + default configurations (#3)

- Add files sigv4.h and sigv4_config_defaults.h
- Add public-facing API elements detailed in design doc

Format Date Header for ISO8601 Compliance (#4)

Add optional utility function to format date header returned from AWS IoT (ex. in temp tokens) for compliance with the ISO8601 format required for authentication

Add unit tests for SigV4_AwsIotDateToIso8601() (#8)

Setup proof infrastructure for CBMC (#7)

* Add Litani and templates for CBMC

* Add sample proof

* Implement CBMC proof for SigV4_AwsIotDateToIso8601

* Unwind all loops such that no unwinding errors occur

Change submodule to use https rather than ssh for aws-templates-for-cbmc-proofs (#12)

* CBMC fix test (do not merge)

* Change AWS templates to https instead of ssh

* Revert README

Update README.md and LICENSE files (#14)

Update README.md and LICENSE files before changing repo's visibility status (to public).

Add remaining doxygen + link verification checks (#15)

Add doxygen + link verifier checks (the library-specific doxygen content will be added in a separate PR for further review).

[SigV4] CBMC proof for Sigv4_awsIotdatetoISO8601 API (#19)

* Sigv4_AWSIOtDateToISO8601 CBMC PROOF

* Unit test coverage changes

Add release workflow (+ revert to previous license) (#18)

change permissions of run_cbmc_proofs.py (#21)

[Sigv4] Doxygen content updates (#22)

* doxygen doc update

* lexicon update

Update proof tools (+disable submodule cloning by default) (#20)

This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:

- Profiling
    - Litani measures the memory usage of the CBMC safety checking and
      coverage checking jobs
    - The dashboard includes box-and-whisker diagrams for memory use per
      proof
    - The dashboard includes a graph of how many parallel jobs are
      running over the whole run, making it easy to choose a CI machine
      with enough parallelism
    - It is now possible to designate particular proofs as "EXPENSIVE";
      Litani runs expensive proofs serially, ensuring that they do not
      over-consume resources like RAM.

- UI improvements
    - Each pipeline page includes a table of contents
    - Each pipeline page includes a dependency graph of the pipeline
    - Each job on the pipeline page has a hyperlink to that job
    - The terminal output is now less noisy

SigV4_GenerateHTTPAuthorization() API Functionality (#16)

* Squash of outdated #13 commits

* Hold for checks

* Add definitions for sorting structures

* Include parsing functions

* Fix old commit error

* Missing asserts

* (temporarily allow warnings)

* Spell check + include partial context

* More updates to lexicon+doxygen

* Add asserts for private func.

* Move access after asserts

* Clarify pointer increment

* Update postfix syntax for correct operator precedence

* Feedback changes only

* + remove accidental duplicate

Implement credential scope

Implement generate credential query

Validation of parameter count

Solution a bit overcomplicated

Squash bugs and canonical query parameters should also be sorted by value

Finish canonicalize query

Fix canonical URI encoding

Add hash helper function

Add hmac implementation

Add newline chars for canonical request

Finish writing of canonical request

Hex-encoded hash of canonical request matches

Write string to sign

Fix bug

Refactor writeStringToSign for complexity

Allow HMAC keys to be passed through separate function calls

Add code for generating signing key

Fix hmac bug

Generate the final signature correctly

Fix bug

Fix newline not being written

Merge Shivangi's code

Stylistic changes

Link OpenSSL to the test

Add unit tests attaining branch coverage of 71%

Integrate Shivangi's latest changes

Output authBufLen when complete

Update logic when headers are precanonicalized.

Add additional parameter checks for block/digest len

Add documentation

Fix test case

Get complexity <= 8 for private functions

Reduce complexity

Remove use of %zu

Revert changes to test as it was added to another PR

Uncrustify and add doxygen strings.

Add docs

Resolve doxygen errors and lexicon.txt

Document all private functions

Fix remaining doxygen errors

Update lexicon.txt

Remove duplicate declaration

Remove assertions on pQuery being NULL

Add log messages for insufficient memory errors

Uncrustify

* Merge doxygen

* Create SigV4ConstString_t type

* Fix checks

* Hygiene improvements in URI encoding logic

* Hygiene improvements in Authorization Header prefix value logic

* Minor improvements

* Resolve compiler warning

* Fix checks

* Address review comments

* More comment changes

* Fix build errors

* Fix unit test run failures

* Add test case for sorting corner cases

* Minor coverage increment and hygiene of redundant length check in library

* Prune API to remove unused members of struct, and add test coverage for input parameter validation

* More code coverage on logic of trimmable spaces & header count > threshold

* Hygiene improvements in build configuration

* Small refactor in implementation and complete testing coverage of encodeURI

* Fix bugs in encodeURI implementation when handling special characters or double encoded equals sign

* Fix some CI checks

* Disable asserts from unit test coverage

* Fix some doxygen failures

* Address minor review comments

* Add error code for invalid HTTP headers and increment test coverage

* Hygiene improvement in sigv4.c and test coverage increment

* Minor hygiene refactor in implementation and test coverage for canonical query logic

* Complete test coverage for canonical functions

* Fix some CI check failures

* Make more hygiene improvements and increase test coverage

* Achieve 100% coverage

* Hygiene improvements

* Minor README.md update

* Address review comments

* Quicksort: Remove unnecessary branches of invalid array or elements and add helpful comments

* 100% coverage again

* Apply suggestions from code review

Co-authored-by: Oscar Michael Abrina <[email protected]>
Co-authored-by: Muneeb Ahmed <[email protected]>

* Fix complexity and hygiene improvements

Co-authored-by: Archit Aggarwal <[email protected]>
Co-authored-by: Muneeb Ahmed <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants