Add CN specs to MKM #142
Add CN specs to MKM #142
Conversation
spernsteiner
force-pushed
the
98-mkm-server
branch
from
5a2dcc7 to
0e65e31
Compare
septract
force-pushed
the
139-feature-verify-test-mkm-module
branch
from
667e47c to
a4f9a2a
Compare
septract
force-pushed
the
139-feature-verify-test-mkm-module
branch
from
a4f9a2a to
218a2f2
Compare
|
@peterohanley @podhrmic PR ready to be re-reviewed when you have time. We now supports verification and functional correctness proofs of MKM, and testing of MKM. I've removed a lot of the limitations that existed before (but introduced some new ones caused by the test generator...). |
This is due to cerberus issue 437. The CN_TEST definition is not enough, we would need another definition so that CN sees them but they are not in the code passed to cc.
|
I fixed the CI errors from the |
| int client_epoll_ctl(struct client* c, int epfd, int op) { | ||
| int client_epoll_ctl(struct client* c, int epfd, int op) | ||
| /*$ | ||
| // TODO fill in an actual spec here, depending what's needed |
There was a problem hiding this comment.
@septract please either provide specs, or explain why we are not providing them (e.g. unsupported by the CN)
| let pos = (u64) Client_in.pos; | ||
| ensures | ||
| take Client_out = ClientObject(c); | ||
| // TODO more compact notation? |
There was a problem hiding this comment.
@septract please remove the TODOs, or add explanation why we still have those
| @@ -133,7 +261,15 @@ enum client_event_result client_read(struct client* c) { | |||
| return RES_DONE; | |||
| } | |||
|
|
|||
| int ret = read(c->fd, buf + c->pos, buf_size - c->pos); | |||
| // TODO Mysterious why this particular case split is needed | |||
There was a problem hiding this comment.
@septract is there a ticket filled that captures this mystery?
| @@ -158,7 +303,21 @@ enum client_event_result client_write(struct client* c) { | |||
| return RES_DONE; | |||
| } | |||
|
|
|||
| int ret = write(c->fd, buf + c->pos, buf_size - c->pos); | |||
| // TODO Mysterious why this particular case split is needed | |||
There was a problem hiding this comment.
@septract please remove the TODOs
| ensures | ||
| take Client_out = ClientObject(c); | ||
|
|
||
| // TODO more compact notation needed saying 'all fields except but X remains unchanged' |
There was a problem hiding this comment.
@septract is this captured in a ticket? (CN redesign?)
| uint8_t hmac_message[MEASURE_SIZE + NONCE_SIZE] = {0}; | ||
| // TODO gross hack caused by weird CN type lifting |
There was a problem hiding this comment.
Please provide more context/link to an issue
| @@ -75,7 +179,22 @@ const uint8_t* policy_match(uint8_t key_id[KEY_ID_SIZE], uint8_t nonce[NONCE_SIZ | |||
| } | |||
|
|
|||
| // Now check each policy entry in turn to find one that matches. | |||
| for (size_t i = 0; i < policy_table_len; ++i) { | |||
| // TODO: can't use prefix ++i due to #807 | |||
There was a problem hiding this comment.
| // TODO: can't use prefix ++i due to #807 | |
| // TODO: can't use prefix ++i | |
| // see https://github.com/rems-project/cerberus/issues/807 |
| @@ -85,3 +204,4 @@ const uint8_t* policy_match(uint8_t key_id[KEY_ID_SIZE], uint8_t nonce[NONCE_SIZ | |||
| fprintf(stderr, "policy_match: no match\n"); | |||
| return NULL; | |||
| } | |||
| #endif | |||
There was a problem hiding this comment.
| #endif | |
| #endif | |
| /*$ function (u64) KEY_SIZE () $*/ | ||
| static uint64_t c_KEY_SIZE() /*$ cn_function KEY_SIZE; $*/ { return KEY_SIZE; } | ||
| #else | ||
| // TODO: Have to hardcode the values as CN test doesn't support cn_function :( |
There was a problem hiding this comment.
Link to an issue please...
| @@ -31,6 +59,7 @@ int policy_add( | |||
| const uint8_t key_id[KEY_ID_SIZE], | |||
| const uint8_t measure[MEASURE_SIZE], | |||
| const uint8_t key[KEY_SIZE]); | |||
| // TODO: can't write a spec here thanks to #371 | |||
There was a problem hiding this comment.
| // TODO: can't write a spec here thanks to #371 | |
| // TODO: can't write a spec here, see https://github.com/rems-project/cerberus/issues/371 |
|
I've fixed the TODOs in @podhrmic how does that sound? |
|
Thanks for the changes @septract ! I am a bit hesitant to keep a separate branch as it makes the OpenSUT delivery more difficult. Maybe merge as is and deal with the TODOs later? |
This PR adds CN functional specifications to the MKM code in
client.c, as well as various supporting files. These specifications are intended to be run-time tested as well as verified.Files:
client.c- target function definitionsclient.h- types, and CN predicates defining the typescn_stubs.h- specifications and redefinitions for various library functions that can't be supported directlyrun-cn-test.sh- run the CN test generator using the necessary flagsprocess-cn-test.sh- run the preprocessor. Called byrun-cn-test.shUnfortunately, the CN verifier and test generators require different code-level annotations at various points. We handle this using a pair of macros:
CN_ENV- set when calling CN in either verify or test modesCN_TEST- set when calling CN in test modeTesting the PR
To run the verifier, run:
Note this may be quite slow. It takes around 3m30s to complete on my newish MBP.
To run the tests, run:
Outstanding bugs
TheFIXEDrun-cn-test.shscript pauses during execution and only continues when I pressreturn. I assume this is due to some call inclient.cwhich is blocking, but I haven't figured out the culprit yet.TODOnotes. These generally indicate places I'm working around a limitation in CN of some kind. But some of these might be possible to resolve.Changes: