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.

Sign up for GitHub

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

Jump to bottom

Cryptol property to implementation property coverage #87

Open
3 tasks
kiniry opened this issue Feb 18, 2022 · 0 comments
Open
3 tasks

Cryptol property to implementation property coverage #87

kiniry opened this issue Feb 18, 2022 · 0 comments
Labels
ACSL Matters related to ACSL specifications and/or the use of Frama-C. assurance Issues that relate to the assurance of the system, whether via models, code, informal, or formal. cryptol Issues related to our Cryptol specifications, or use thereof. documentation Issues that relate to documentation about the system, including user and developer docs, source code ENHANCEMENT New feature or request On Deck Q/A Quality assurance issue; validation, testing, and formal assurance. software Someday Issues that are not required by our current contract, but we'd like to attend to someday. source code Issues that relate to source code implementation. specifications Issues that relate to system specifications, whether of models, code, protocols, or otherwise. verification
Milestone
Assurance

Comments

@kiniry
Copy link
Member

kiniry commented Feb 18, 2022

Ensure that we have translated, in a traceable fashion, a refinement of every Cryptol property to:

  1. An ACSL assertion that is checkable in one or more ways by Frama-C plug-ins.
  2. A SAWscript relation or assertion that is checkable by SAW.
  3. A test bench/verification bench property that is checkable in one or more ways with some combination of runtime verification on executable models, digital twins, or the final hardware platform.

Our final assurance matrix should include a checklist of such refinements and evidence.
@kiniry kiniry added documentation Issues that relate to documentation about the system, including user and developer docs, source code ENHANCEMENT New feature or request specifications Issues that relate to system specifications, whether of models, code, protocols, or otherwise. software verification On Deck assurance Issues that relate to the assurance of the system, whether via models, code, informal, or formal. Q/A Quality assurance issue; validation, testing, and formal assurance. source code Issues that relate to source code implementation. cryptol Issues related to our Cryptol specifications, or use thereof. ACSL Matters related to ACSL specifications and/or the use of Frama-C. labels Feb 18, 2022
@kiniry kiniry added this to the Task 3: Evaluation milestone Feb 18, 2022
@kiniry kiniry removed this from the Task 3: Evaluation milestone Oct 28, 2022
@kiniry kiniry added the Someday Issues that are not required by our current contract, but we'd like to attend to someday. label Oct 28, 2022
@kiniry kiniry added this to the Assurance milestone May 22, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
ACSL Matters related to ACSL specifications and/or the use of Frama-C. assurance Issues that relate to the assurance of the system, whether via models, code, informal, or formal. cryptol Issues related to our Cryptol specifications, or use thereof. documentation Issues that relate to documentation about the system, including user and developer docs, source code ENHANCEMENT New feature or request On Deck Q/A Quality assurance issue; validation, testing, and formal assurance. software Someday Issues that are not required by our current contract, but we'd like to attend to someday. source code Issues that relate to source code implementation. specifications Issues that relate to system specifications, whether of models, code, protocols, or otherwise. verification
Projects
None yet
Milestone
Assurance
Development

No branches or pull requests
1 participant
@kiniry