Skip to content

Commit 2cd97d5

Browse files
gebnergebner
committed
Port DPE example from prototype.
1 parent 23c4f03 commit 2cd97d5

8 files changed

Lines changed: 446 additions & 0 deletions

File tree

‎examples/dpe/DPE.c‎

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
#include <stdlib.h>
2+
#include <stdint.h>
3+
#include <stdbool.h>
4+
#include "DPE.h"
5+
#include "EngineCore.h"
6+
7+
_include_pulse(
8+
$declare(context_t s)
9+
[@@erasable]
10+
noeq type context_full_data =
11+
| PL_Engine of (Seq.seq UInt8.t)
12+
| PL_L0 of (Seq.seq UInt8.t)
13+
| PL_L1 // tbd
14+
15+
let tag_relation ($(s): $type(context_t)) (h: context_full_data) : prop =
16+
match $(s.tag) with
17+
| 0uy -> Field__u_context_t__uds? $(s.payload) /\ PL_Engine? h
18+
| 1uy -> Field__u_context_t__cdi? $(s.payload) /\ PL_L0? h
19+
| 2uy -> Field__u_context_t__l1_context? $(s.payload) /\ PL_L1? h
20+
| _ -> False
21+
)
22+
23+
_include_pulse(
24+
$declare(context_t s)
25+
26+
let context_full_pred ([@@@mkey] $(s): $type(context_t)) (h: context_full_data) : slprop =
27+
match $(s.payload), h with
28+
| Field__u_context_t__uds uds_ptr, PL_Engine uds_data ->
29+
uds_ptr |-> uds_data ** freeable_array uds_ptr
30+
| Field__u_context_t__cdi cdi_ptr, PL_L0 cdi_data ->
31+
cdi_ptr |-> cdi_data ** freeable_array cdi_ptr
32+
| Field__u_context_t__l1_context _, PL_L1 ->
33+
emp
34+
| _ -> pure False
35+
36+
let engine_state ($(s): $type(context_t)) #x =
37+
observe (context_full_pred $(s)) #x
38+
39+
ghost fn elim_context_full_pred_uds ($(s): $type(context_t)) (#h: context_full_data)
40+
requires with_pure (tag_relation $(s) h /\ PL_Engine? h)
41+
requires context_full_pred $(s) h
42+
ensures Pulse.Lib.Array.pts_to $(s.payload.uds) (PL_Engine?._0 h)
43+
ensures freeable_array $(s.payload.uds)
44+
{
45+
unfold context_full_pred;
46+
rewrite each $(s.payload) as Field__u_context_t__uds $(s.payload.uds);
47+
rewrite each h as PL_Engine (PL_Engine?._0 h);
48+
}
49+
50+
ghost fn elim_context_full_pred_cdi ($(s): $type(context_t)) (#h: context_full_data)
51+
requires with_pure (tag_relation $(s) h /\ PL_L0? h)
52+
requires context_full_pred $(s) h
53+
ensures Pulse.Lib.Array.pts_to $(s.payload.cdi) (PL_L0?._0 h)
54+
ensures freeable_array $(s.payload.cdi)
55+
{
56+
unfold context_full_pred;
57+
rewrite each $(s.payload) as Field__u_context_t__cdi $(s.payload.cdi);
58+
rewrite each h as PL_L0 (PL_L0?._0 h);
59+
}
60+
61+
ghost fn elim_context_full_pred_l1 ($(s): $type(context_t)) (#h: context_full_data)
62+
requires with_pure (tag_relation $(s) h /\ PL_L1? h)
63+
requires context_full_pred $(s) h
64+
{
65+
unfold context_full_pred;
66+
rewrite each $(s.payload) as Field__u_context_t__l1_context $(s.payload.l1_context);
67+
rewrite each h as PL_L1;
68+
}
69+
70+
ghost fn intro_context_full_pred_uds ($(s): $type(context_t)) #uds
71+
requires with_pure (tag_relation $(s) (PL_Engine uds))
72+
requires Pulse.Lib.Array.pts_to $(s.payload.uds) uds
73+
requires freeable_array $(s.payload.uds)
74+
ensures context_full_pred $(s) (PL_Engine uds)
75+
{
76+
rewrite $(s.payload.uds) |-> uds ** freeable_array $(s.payload.uds)
77+
as context_full_pred $(s) (PL_Engine uds);
78+
}
79+
80+
ghost fn intro_context_full_pred_cdi ($(s): $type(context_t)) #cdi
81+
requires with_pure (tag_relation $(s) (PL_L0 cdi))
82+
requires Pulse.Lib.Array.pts_to $(s.payload.cdi) cdi
83+
requires freeable_array $(s.payload.cdi)
84+
ensures context_full_pred $(s) (PL_L0 cdi)
85+
{
86+
rewrite $(s.payload.cdi) |-> cdi ** freeable_array $(s.payload.cdi)
87+
as context_full_pred $(s) (PL_L0 cdi);
88+
}
89+
)
90+
91+
void memcpy_(size_t len, _array const uint8_t *a1, _array uint8_t *a2)
92+
_preserves(a1._length == len)
93+
_preserves(a2._length == len)
94+
_ensures((_slprop) _inline_pulse(rewrites_to (value_of $(a2)) (value_of $(a1))))
95+
{
96+
_ghost_stmt(admit());
97+
}
98+
99+
void free_(_consumes _allocated_array _array uint8_t *arr)
100+
{
101+
_ghost_stmt(admit());
102+
}
103+
104+
_refine((_slprop) _inline_pulse(
105+
exists* state.
106+
pure (tag_relation $(*this) state) **
107+
context_full_pred $(*this) state))
108+
typedef context_t *context_obj;
109+
110+
_allocated
111+
typedef context_obj allocated_context_obj;
112+
allocated_context_obj init_engine_context(const uds_array uds)
113+
_ensures((bool) _inline_pulse(engine_state $(*return) == PL_Engine (value_of $(uds))))
114+
{
115+
uint8_t *uds_buf = (uint8_t*)calloc(UDS_LEN, sizeof(uint8_t));
116+
memcpy_(UDS_LEN, uds, uds_buf);
117+
context_t *ctx = (context_t*)malloc(sizeof(context_t));
118+
*ctx = (context_t) {
119+
.tag = ENGINE_CONTEXT,
120+
.payload = (u_context_t) { .uds = uds_buf },
121+
};
122+
_ghost_stmt(intro_context_full_pred_uds $(*ctx));
123+
return ctx;
124+
}
125+
126+
_include_pulse (
127+
ghost fn elim_maybe_true (p:slprop)
128+
requires maybe _true_ p
129+
ensures p
130+
{ unfold maybe; }
131+
)
132+
133+
void init_l0_context(context_obj ctx, const dice_digest cdi)
134+
_requires((bool) _inline_pulse(PL_Engine? (engine_state $(*ctx))))
135+
_ensures((bool) _inline_pulse(engine_state $(*ctx) == PL_L0 (value_of $(cdi))))
136+
{
137+
uint8_t *cdi_buf = (uint8_t*)calloc(DICE_DIGEST_LEN, sizeof(uint8_t));
138+
memcpy_(DICE_DIGEST_LEN, cdi, cdi_buf);
139+
_ghost_stmt(elim_context_full_pred_uds $(*ctx));
140+
uint8_t* uds_buf = ctx->payload.uds;
141+
free_(uds_buf);
142+
ctx->tag = 1;
143+
ctx->payload.cdi = cdi_buf;
144+
_ghost_stmt(intro_context_full_pred_cdi $(*ctx));
145+
return;
146+
}
147+
148+
void destroy_uds_context(_consumes _allocated context_obj ctx)
149+
_requires(ctx->tag == 0)
150+
{
151+
_ghost_stmt(elim_context_full_pred_uds $(*ctx));
152+
uint8_t* uds_buf = ctx->payload.uds;
153+
free_(uds_buf);
154+
free(ctx);
155+
return;
156+
}
157+
158+
void mk_l0_context(context_obj ctx, _consumes _allocated_array dice_digest cdi)
159+
_requires(ctx->tag == 0)
160+
_ensures((bool) _inline_pulse(engine_state $(*ctx) == PL_L0 (old (value_of $(cdi)))))
161+
{
162+
_assert(cdi._length == DICE_DIGEST_LEN);
163+
_ghost_stmt(elim_context_full_pred_uds $(*ctx));
164+
uint8_t* uds_buf = ctx->payload.uds;
165+
free_(uds_buf);
166+
ctx->tag = 1;
167+
ctx->payload.cdi = cdi;
168+
_ghost_stmt(intro_context_full_pred_cdi $(*ctx));
169+
}
170+
171+
bool derive_child_from_context(context_obj ctx, const engine_record_t *record)
172+
_requires(ctx->tag == 0)
173+
_ensures(return ==> (bool) _inline_pulse(PL_L0? (engine_state $(*ctx))))
174+
_ensures(!return ==> (bool) _inline_pulse(engine_state $(*ctx) == old (engine_state $(*ctx))))
175+
{
176+
_ghost_stmt(elim_context_full_pred_uds $(*ctx));
177+
uint8_t *cdi_buf = (uint8_t*)calloc(DICE_DIGEST_LEN, sizeof(uint8_t));
178+
// _assert(cdi_buf._length == DICE_DIGEST_LEN);
179+
bool ok = false; // engine_main(cdi_buf, ctx->payload.uds, record);
180+
if (ok) {
181+
_ghost_stmt(intro_context_full_pred_uds $(*ctx));
182+
mk_l0_context(ctx, cdi_buf);
183+
return true;
184+
} else {
185+
_ghost_stmt(intro_context_full_pred_uds $(*ctx));
186+
free_(cdi_buf);
187+
return false;
188+
}
189+
}

‎examples/dpe/DPE.h‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
#ifndef _DPE_H_
2+
#define _DPE_H_
3+
4+
#include <stdlib.h>
5+
#include <stdint.h>
6+
#include <stdbool.h>
7+
#include "c2pulse.h"
8+
9+
#define _allocated_array _refine((_slprop) _inline_pulse(freeable_array $(this)))
10+
11+
#define DICE_DIGEST_LEN 64 //TODO generalize
12+
_refine(this._length == DICE_DIGEST_LEN) _array
13+
typedef uint8_t *dice_digest;
14+
15+
16+
#include "HACL.h"
17+
18+
#define UDS_LEN 32
19+
_refine(this._length == UDS_LEN) _array
20+
typedef uint8_t *uds_array;
21+
22+
23+
#define DICE_SUCCESS 0
24+
#define DICE_ERROR 1
25+
#define SHA2_256 0 //maybe use an enum for this?
26+
#define DICE_HASH_ALG SHA2_256
27+
28+
_refine(this.l0_image_header._length == this.l0_image_header_size)
29+
_refine(this.l0_binary._length == this.l0_binary_size)
30+
typedef struct _engine_record_t {
31+
size_t l0_image_header_size;
32+
_array uint8_t *l0_image_header;
33+
ed25519_sig l0_image_header_sig;
34+
size_t l0_binary_size;
35+
_array uint8_t *l0_binary;
36+
dice_digest l0_binary_hash;
37+
ed25519_key l0_image_auth_pubkey;
38+
} engine_record_t;
39+
40+
_refine(this.deviceIDCSR._length == this.deviceIDCSR_len)
41+
_refine(this.aliasKeyCRT._length == this.aliasKeyCRT_len)
42+
typedef struct {
43+
ed25519_key deviceID_pub;
44+
ed25519_key aliasKey_priv;
45+
ed25519_key aliasKey_pub;
46+
size_t deviceIDCSR_len;
47+
_array uint8_t *deviceIDCSR;
48+
size_t aliasKeyCRT_len;
49+
_array uint8_t *aliasKeyCRT;
50+
} l1_context_t;
51+
52+
#define ENGINE_CONTEXT 0
53+
#define L0_CONTEXT 1
54+
#define L1_CONTEXT 2
55+
56+
typedef union _u_context_t {
57+
uds_array uds;
58+
dice_digest cdi;
59+
l1_context_t l1_context;
60+
} u_context_t;
61+
62+
typedef struct {
63+
uint8_t tag;
64+
u_context_t payload;
65+
} context_t;
66+
#endif

‎examples/dpe/DPETypes.c‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
#include <stddef.h>
2+
#include <stdlib.h>
3+
#include <stdio.h>
4+
#include <stdint.h>
5+
#include "c2pulse.h"
6+
#include <stdbool.h>
7+
8+
9+
typedef struct _profile_descriptor_t {
10+
char* name;
11+
uint32_t dpe_spec_version;
12+
uint32_t max_message_size;
13+
bool uses_multi_part_messages;
14+
bool supports_concurrent_operations;
15+
bool supports_encrypted_sessions;
16+
bool supports_derived_sessions;
17+
size_t max_sessions;
18+
char *session_protocol;
19+
bool supports_session_sync;
20+
char *session_sync_policy;
21+
char *session_migration_protocol;
22+
bool supports_default_context;
23+
bool supports_context_handles;
24+
size_t max_contexts_per_session;
25+
size_t max_context_handle_size;
26+
bool supports_auto_init;
27+
bool supports_simulation;
28+
bool supports_attestation;
29+
bool supports_sealing;
30+
bool supports_get_profile;
31+
bool supports_open_session;
32+
bool supports_close_session;
33+
bool supports_sync_session;
34+
bool supports_export_session;
35+
bool supports_import_session;
36+
bool supports_init_context;
37+
bool supports_certify_key;
38+
bool supports_sign;
39+
bool supports_seal;
40+
bool supports_unseal;
41+
bool supports_sealing_public;
42+
bool supports_rotate_context_handle;
43+
char *dice_derivation;
44+
char *asymmetric_derivation;
45+
char *symmetric_derivation;
46+
bool supports_any_label;
47+
char *supported_labels;
48+
char *initial_derivation;
49+
char *input_format;
50+
bool supports_internal_inputs;
51+
bool supports_internal_dpe_info;
52+
bool supports_internal_dpe_dice;
53+
char *internal_dpe_info_type;
54+
char *internal_dpe_dice_type;
55+
char *internal_inputs;
56+
bool supports_certificates;
57+
size_t max_certificate_size;
58+
size_t max_certificate_chain_size;
59+
bool appends_more_certificates;
60+
bool supports_certificate_policies;
61+
bool supports_policy_identity_init;
62+
bool supports_policy_identity_loc;
63+
bool supports_policy_attest_init;
64+
bool supports_policy_attest_loc;
65+
bool supports_policy_assert_init;
66+
bool supports_policy_assert_loc;
67+
char *certificate_policies;
68+
bool supports_eca_certificates;
69+
char* eca_certificate_format;
70+
char *leaf_certificate_format;
71+
char *public_key_format;
72+
bool supports_external_key;
73+
char *to_be_signed_format;
74+
char *signature_format;
75+
bool supports_symmetric_sign;
76+
bool supports_asymmetric_unseal;
77+
bool supports_unseal_policy;
78+
char *unseal_policy_format;
79+
} profile_descriptor_t;
80+
81+

0 commit comments

Comments
 (0)