proof: starting support for e-acsl runtime assertion as advanced security mode #34
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
3 times, most recently
from
76108da to
e3ff20e
Compare
PThierry
changed the title
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
from
e3ff20e to
6ffbc91
Compare
PThierry
added
question
NOTE: need CEA support on this
fixing e-acsl call with fewer checks
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
from
f3878bb to
2b0ab26
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR enables the support for generated annotated C code using e-acsl based on the various ACSL assertions written in the input C file.
The ability to add e-acsl annotations is supported kernel-wide and is made to be enabled easily.
By now, the kernel zlib's string.c implementation of memset/memcpy/strnlen do support e-acsl annotations.
Triggering the annotated C code generation and inclusion is made based on the
CONFIG_SECU_ENABLE_EACSLkconfig trigger (default n).In that very case, Frama-C, including the e-acsl plugin and the
e-acsl-gcc.shtool, generates annotated sources that allow automatically runtime assertion checks baed on static frama-C assertions, that have been proven as valid in a sound model.As a consequence, any invalid runtime assertion can't be triggered through a valid logical path and is the consequence of an external event (EM, fault).
runtime annotations increase the kernel size, and is deactivated by default. By now, only the string memory manipulation library is protected (as already validated as correct in a sound envionrment), but such runtime assertions can be generated to any code part that is already demonstrated as correct without risk.
NOTE: need CEA support on this, ass the e-acsl plugin C symbols implementation library need to be compiled and linked