https://github.com/awslabs/aws-verification-model-for-libcrypto
Partial verification model for openssl.
https://github.com/awslabs/aws-verification-model-for-libcrypto
Science Score: 26.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
○CITATION.cff file
-
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (9.6%) to scientific vocabulary
Repository
Partial verification model for openssl.
Basic Info
Statistics
- Stars: 5
- Watchers: 7
- Forks: 18
- Open Issues: 5
- Releases: 0
Metadata Files
README.md
AWS Verification Model For LibCrypto
Formal verification tools, such as CBMC, often require "verification models" of libraries in order to verify code that uses these libraries. These models provide an abstract implementation of the library API, as opposed to the concrete implementation the library itself provides. For example, the concrete implementation of a hash-function might invoke a complicated cryptographic routine. The abstract implementation, on the other hand, might simply assert that the pointers given are valid, and then return an "unconstrained" (AKA "non-deterministic") value. This allows verification tools to focus on the contracts guaranteed by the API, without having to spend time and memory analyzing the detailed implementation. It also helps make proofs robust against changes to the library implementation: as long as the library continues to implement the API described in the model, the proof will hold, even if the library changes.
This repository contains a partial verification model for libCrypto. In particular, it contains abstract models, written in C, of the particular functions used by projects that we have verified. We do not currently cover all, or even most, of the libCrypto API. And we do not cover all the functionality of the API that we do cover - in many cases, we model just enough to enable the proofs of other projects to go through.
We welcome contributions modelling the remaining libCrypto functionality.
Security
See CONTRIBUTING for more information.
License
This project is licensed under the Apache-2.0 License.
Owner
- Name: Amazon Web Services - Labs
- Login: awslabs
- Kind: organization
- Location: Seattle, WA
- Website: http://amazon.com/aws/
- Repositories: 914
- Profile: https://github.com/awslabs
AWS Labs
GitHub Events
Total
- Issue comment event: 1
- Push event: 2
- Pull request review event: 12
- Pull request review comment event: 11
- Pull request event: 5
Last Year
- Issue comment event: 1
- Push event: 2
- Pull request review event: 12
- Pull request review comment event: 11
- Pull request event: 5
Issues and Pull Requests
Last synced: 10 months ago
All Time
- Total issues: 6
- Total pull requests: 40
- Average time to close issues: about 1 month
- Average time to close pull requests: about 19 hours
- Total issue authors: 3
- Total pull request authors: 10
- Average comments per issue: 0.33
- Average comments per pull request: 0.13
- Merged pull requests: 32
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 3
- Average time to close issues: N/A
- Average time to close pull requests: about 18 hours
- Issue authors: 0
- Pull request authors: 3
- Average comments per issue: 0
- Average comments per pull request: 0.33
- Merged pull requests: 1
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
- feliperodri (4)
- adpaco-aws (1)
- SaswatPadhi (1)
Pull Request Authors
- feliperodri (17)
- danielsn (8)
- nwetzler (3)
- jimgrundy (2)
- SaswatPadhi (2)
- tautschnig (2)
- lrstewart (2)
- goatgoose (2)
- jouho (1)
- jmayclin (1)
- tegansb (1)
Top Labels
Issue Labels
Pull Request Labels
Dependencies
- DoozyX/clang-format-lint-action v0.5 composite
- actions/checkout v2 composite