Skip to content

Panic freedom with F* #133

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

Closed
wants to merge 30 commits into from
Closed

Panic freedom with F* #133

Show file tree
Hide file tree
Changes from 28 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
0bf761a
getting fstar to verify without patches
karthikbhargavan Jan 12, 2025
a2515dd
wip: panic freedom
karthikbhargavan Jan 14, 2025
c00e4ce
fsti
karthikbhargavan Jan 15, 2025
df9e597
pushing formats
karthikbhargavan Jan 15, 2025
3583640
Merge branch 'main' into fstar-fixes
karthikbhargavan Jan 16, 2025
ba07f35
fmt
karthikbhargavan Jan 16, 2025
3964f3e
secret integer fix
karthikbhargavan Jan 16, 2025
64a2505
cfg hax
karthikbhargavan Jan 16, 2025
aed4d9c
cfg hax
karthikbhargavan Jan 16, 2025
0ef31c7
cfg hax
karthikbhargavan Jan 16, 2025
f12e2c3
lint
karthikbhargavan Jan 16, 2025
213ade1
Merge branch 'main' into fstar-fixes
karthikbhargavan Jan 16, 2025
ada6daa
Merge branch 'main' into fstar-fixes
karthikbhargavan Mar 9, 2025
33c77fa
Merge branch 'main' into fstar-fixes
karthikbhargavan Mar 9, 2025
5bc4ef3
regen
karthikbhargavan Mar 9, 2025
a7d17ea
hand edits
karthikbhargavan Mar 9, 2025
de1b1e4
progress
karthikbhargavan Mar 9, 2025
a99f765
wip
karthikbhargavan Mar 9, 2025
731cafe
parse client hello progress
karthikbhargavan Mar 9, 2025
f8a4b56
formats panic free
karthikbhargavan Mar 9, 2025
b1acf10
added post conditions for handshake data
karthikbhargavan Mar 9, 2025
3889bc7
passed handshake
karthikbhargavan Mar 9, 2025
e480b43
record wip
karthikbhargavan Mar 9, 2025
d432e00
fewer hand edits
karthikbhargavan Mar 10, 2025
3ffa7ca
removed hand edits (except let rec bug) using decreases
karthikbhargavan Mar 10, 2025
1f7ebb0
no hand edits
karthikbhargavan Mar 11, 2025
ab8a230
removed self_ hacks
karthikbhargavan Mar 11, 2025
237ca24
Merge branch 'main' into fstar-fixes
karthikbhargavan Mar 11, 2025
c835c63
wip
karthikbhargavan Mar 20, 2025
46a08ad
fig
karthikbhargavan Apr 8, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion hax-driver.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ def shell(command, expect=0, cwd=None, env={}):
"-**::non_hax::** -bertie::stream::**",
"fstar",
"--interfaces",
"+** +!bertie::tls13crypto::** +!bertie::tls13utils::**",
"+** +!bertie::tls13crypto::** +!bertie::tls13utils::** +!bertie::tls13cert::**"
],
cwd=".",
env=hax_env,
Expand Down
194 changes: 96 additions & 98 deletions proofs/fstar/extraction/Bertie.Tls13api.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,27 +30,26 @@ let in_psk_mode (c: t_Client) =
Bertie.Tls13crypto.t_Algorithms)

let impl_Client__connect
(#iimpl_916461611_: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Rand_core.t_CryptoRng iimpl_916461611_)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Rand_core.t_RngCore iimpl_916461611_)
(#iimpl_447424039_: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Rand_core.t_CryptoRng iimpl_447424039_)
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(server_name: Bertie.Tls13utils.t_Bytes)
(session_ticket psk: Core.Option.t_Option Bertie.Tls13utils.t_Bytes)
(rng: iimpl_916461611_)
(rng: iimpl_447424039_)
=
let tmp0, out:(iimpl_916461611_ &
let tmp0, out:(iimpl_447424039_ &
Core.Result.t_Result
(Bertie.Tls13formats.Handshake_data.t_HandshakeData &
Core.Option.t_Option Bertie.Tls13record.t_ClientCipherState0 &
Bertie.Tls13handshake.t_ClientPostClientHello) u8) =
Bertie.Tls13handshake.client_init #iimpl_916461611_
Bertie.Tls13handshake.client_init #iimpl_447424039_
ciphersuite
server_name
session_ticket
psk
rng
in
let rng:iimpl_916461611_ = tmp0 in
let rng:iimpl_447424039_ = tmp0 in
match
out
<:
Expand Down Expand Up @@ -81,19 +80,19 @@ let impl_Client__connect
in
rng, hax_temp_output
<:
(iimpl_916461611_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
(iimpl_447424039_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
| Core.Result.Result_Err err ->
rng,
(Core.Result.Result_Err err
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
<:
(iimpl_916461611_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8))
(iimpl_447424039_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8))
| Core.Result.Result_Err err ->
rng,
(Core.Result.Result_Err err <: Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
<:
(iimpl_916461611_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
(iimpl_447424039_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)

let impl_Client__read_handshake (self: t_Client) (handshake_bytes: Bertie.Tls13utils.t_Bytes) =
match self <: t_Client with
Expand Down Expand Up @@ -266,14 +265,89 @@ let impl_Client__write (self: t_Client) (application_data: Bertie.Tls13utils.t_A
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8

let impl_Server__read_handshake (self: t_Server) (handshake_bytes: Bertie.Tls13utils.t_Bytes) =
match self <: t_Server with
| Server_ServerH sstate e_cipher0 cipher_hs cipher1 ->
(match
Bertie.Tls13record.decrypt_handshake handshake_bytes cipher_hs
<:
Core.Result.t_Result
(Bertie.Tls13formats.Handshake_data.t_HandshakeData &
Bertie.Tls13record.t_DuplexCipherStateH) u8
with
| Core.Result.Result_Ok (cf, e_cipher_hs) ->
(match
Bertie.Tls13handshake.server_finish cf sstate
<:
Core.Result.t_Result Bertie.Tls13handshake.t_ServerPostClientFinished u8
with
| Core.Result.Result_Ok sstate ->
Core.Result.Result_Ok (Server_Server1 sstate cipher1 <: t_Server)
<:
Core.Result.t_Result t_Server u8
| Core.Result.Result_Err err ->
Core.Result.Result_Err err <: Core.Result.t_Result t_Server u8)
| Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_Server u8
)
| _ ->
Core.Result.Result_Err Bertie.Tls13utils.v_INCORRECT_STATE <: Core.Result.t_Result t_Server u8

let impl_Server__write (self: t_Server) (application_data: Bertie.Tls13utils.t_AppData) =
match self <: t_Server with
| Server_Server1 sstate cipher1 ->
(match
Bertie.Tls13record.encrypt_data application_data (mk_usize 0) cipher1
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13record.t_DuplexCipherState1)
u8
with
| Core.Result.Result_Ok (v_by, cipher1) ->
Core.Result.Result_Ok
(v_by, (Server_Server1 sstate cipher1 <: t_Server) <: (Bertie.Tls13utils.t_Bytes & t_Server)
)
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Server) u8
| Core.Result.Result_Err err ->
Core.Result.Result_Err err <: Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Server) u8
)
| _ ->
Core.Result.Result_Err Bertie.Tls13utils.v_INCORRECT_STATE
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Server) u8

let impl_Server__read (self: t_Server) (application_data: Bertie.Tls13utils.t_Bytes) =
match self <: t_Server with
| Server_Server1 sstate cipher1 ->
(match
Bertie.Tls13record.decrypt_data application_data cipher1
<:
Core.Result.t_Result (Bertie.Tls13utils.t_AppData & Bertie.Tls13record.t_DuplexCipherState1)
u8
with
| Core.Result.Result_Ok (ad, cipher1) ->
Core.Result.Result_Ok
((Core.Option.Option_Some ad <: Core.Option.t_Option Bertie.Tls13utils.t_AppData),
(Server_Server1 sstate cipher1 <: t_Server)
<:
(Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server))
<:
Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8
| Core.Result.Result_Err err ->
Core.Result.Result_Err err
<:
Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8)
| _ ->
Core.Result.Result_Err Bertie.Tls13utils.v_INCORRECT_STATE
<:
Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8

let impl_Server__accept
(#iimpl_916461611_: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Rand_core.t_CryptoRng iimpl_916461611_)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Rand_core.t_RngCore iimpl_916461611_)
(#iimpl_447424039_: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Rand_core.t_CryptoRng iimpl_447424039_)
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(db: Bertie.Server.t_ServerDB)
(client_hello: Bertie.Tls13utils.t_Bytes)
(rng: iimpl_916461611_)
(rng: iimpl_447424039_)
=
let ch_rec:Bertie.Tls13utils.t_Bytes =
Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve client_hello
Expand All @@ -287,17 +361,17 @@ let impl_Server__accept
Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData u8
with
| Core.Result.Result_Ok ch ->
let tmp0, out:(iimpl_916461611_ &
let tmp0, out:(iimpl_447424039_ &
Core.Result.t_Result
(Bertie.Tls13formats.Handshake_data.t_HandshakeData &
Bertie.Tls13formats.Handshake_data.t_HandshakeData &
Core.Option.t_Option Bertie.Tls13record.t_ServerCipherState0 &
Bertie.Tls13record.t_DuplexCipherStateH &
Bertie.Tls13record.t_DuplexCipherState1 &
Bertie.Tls13handshake.t_ServerPostServerFinished) u8) =
Bertie.Tls13handshake.server_init #iimpl_916461611_ ciphersuite ch db rng
Bertie.Tls13handshake.server_init #iimpl_447424039_ ciphersuite ch db rng
in
let rng:iimpl_916461611_ = tmp0 in
let rng:iimpl_447424039_ = tmp0 in
(match
out
<:
Expand Down Expand Up @@ -335,7 +409,7 @@ let impl_Server__accept
in
rng, hax_temp_output
<:
(iimpl_916461611_ &
(iimpl_447424039_ &
Core.Result.t_Result
(Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)
| Core.Result.Result_Err err ->
Expand All @@ -345,7 +419,7 @@ let impl_Server__accept
Core.Result.t_Result
(Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)
<:
(iimpl_916461611_ &
(iimpl_447424039_ &
Core.Result.t_Result
(Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8))
| Core.Result.Result_Err err ->
Expand All @@ -355,7 +429,7 @@ let impl_Server__accept
Core.Result.t_Result
(Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)
<:
(iimpl_916461611_ &
(iimpl_447424039_ &
Core.Result.t_Result
(Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8))
| Core.Result.Result_Err err ->
Expand All @@ -365,7 +439,7 @@ let impl_Server__accept
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8
)
<:
(iimpl_916461611_ &
(iimpl_447424039_ &
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8
))
| Core.Result.Result_Err err ->
Expand All @@ -374,81 +448,5 @@ let impl_Server__accept
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)
<:
(iimpl_916461611_ &
(iimpl_447424039_ &
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)

let impl_Server__read_handshake (self: t_Server) (handshake_bytes: Bertie.Tls13utils.t_Bytes) =
match self <: t_Server with
| Server_ServerH sstate e_cipher0 cipher_hs cipher1 ->
(match
Bertie.Tls13record.decrypt_handshake handshake_bytes cipher_hs
<:
Core.Result.t_Result
(Bertie.Tls13formats.Handshake_data.t_HandshakeData &
Bertie.Tls13record.t_DuplexCipherStateH) u8
with
| Core.Result.Result_Ok (cf, e_cipher_hs) ->
(match
Bertie.Tls13handshake.server_finish cf sstate
<:
Core.Result.t_Result Bertie.Tls13handshake.t_ServerPostClientFinished u8
with
| Core.Result.Result_Ok sstate ->
Core.Result.Result_Ok (Server_Server1 sstate cipher1 <: t_Server)
<:
Core.Result.t_Result t_Server u8
| Core.Result.Result_Err err ->
Core.Result.Result_Err err <: Core.Result.t_Result t_Server u8)
| Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_Server u8
)
| _ ->
Core.Result.Result_Err Bertie.Tls13utils.v_INCORRECT_STATE <: Core.Result.t_Result t_Server u8

let impl_Server__write (self: t_Server) (application_data: Bertie.Tls13utils.t_AppData) =
match self <: t_Server with
| Server_Server1 sstate cipher1 ->
(match
Bertie.Tls13record.encrypt_data application_data (mk_usize 0) cipher1
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13record.t_DuplexCipherState1)
u8
with
| Core.Result.Result_Ok (v_by, cipher1) ->
Core.Result.Result_Ok
(v_by, (Server_Server1 sstate cipher1 <: t_Server) <: (Bertie.Tls13utils.t_Bytes & t_Server)
)
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Server) u8
| Core.Result.Result_Err err ->
Core.Result.Result_Err err <: Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Server) u8
)
| _ ->
Core.Result.Result_Err Bertie.Tls13utils.v_INCORRECT_STATE
<:
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Server) u8

let impl_Server__read (self: t_Server) (application_data: Bertie.Tls13utils.t_Bytes) =
match self <: t_Server with
| Server_Server1 sstate cipher1 ->
(match
Bertie.Tls13record.decrypt_data application_data cipher1
<:
Core.Result.t_Result (Bertie.Tls13utils.t_AppData & Bertie.Tls13record.t_DuplexCipherState1)
u8
with
| Core.Result.Result_Ok (ad, cipher1) ->
Core.Result.Result_Ok
((Core.Option.Option_Some ad <: Core.Option.t_Option Bertie.Tls13utils.t_AppData),
(Server_Server1 sstate cipher1 <: t_Server)
<:
(Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server))
<:
Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8
| Core.Result.Result_Err err ->
Core.Result.Result_Err err
<:
Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8)
| _ ->
Core.Result.Result_Err Bertie.Tls13utils.v_INCORRECT_STATE
<:
Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8
64 changes: 31 additions & 33 deletions proofs/fstar/extraction/Bertie.Tls13api.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,14 +46,13 @@ val in_psk_mode (c: t_Client) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_T
/// client hello record as bytes, and the [`Client`] state as the second element.
/// If an error occurs, it returns a [`TLSError`].
val impl_Client__connect
(#iimpl_916461611_: Type0)
{| i1: Rand_core.t_CryptoRng iimpl_916461611_ |}
{| i2: Rand_core.t_RngCore iimpl_916461611_ |}
(#iimpl_447424039_: Type0)
{| i1: Rand_core.t_CryptoRng iimpl_447424039_ |}
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(server_name: Bertie.Tls13utils.t_Bytes)
(session_ticket psk: Core.Option.t_Option Bertie.Tls13utils.t_Bytes)
(rng: iimpl_916461611_)
: Prims.Pure (iimpl_916461611_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
(rng: iimpl_447424039_)
: Prims.Pure (iimpl_447424039_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8)
Prims.l_True
(fun _ -> Prims.l_True)

Expand Down Expand Up @@ -111,33 +110,6 @@ type t_Server =
Bertie.Tls13record.t_DuplexCipherState1
-> t_Server

/// Start a new TLS handshake as server.
/// Note that Bertie servers only support a single ciphersuite at a time and
/// do not perform ciphersuite negotiation.
/// This function takes the
/// * `ciphersuite` to use for this server
/// * `db` for the server database containing certificates and keys
/// * `client_hello` for the initial client hello message
/// * `entropy` for the randomness required in the handshake
/// The function returns a [`Result`].
/// When successful, the function returns a three-tuple with the first element the
/// server hello record as bytes, the second the server finished record as bytes,
/// and the new [`Server`] state as the third element.
/// If an error occurs, it returns a [`TLSError`].
val impl_Server__accept
(#iimpl_916461611_: Type0)
{| i1: Rand_core.t_CryptoRng iimpl_916461611_ |}
{| i2: Rand_core.t_RngCore iimpl_916461611_ |}
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(db: Bertie.Server.t_ServerDB)
(client_hello: Bertie.Tls13utils.t_Bytes)
(rng: iimpl_916461611_)
: Prims.Pure
(iimpl_916461611_ &
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)
Prims.l_True
(fun _ -> Prims.l_True)

/// Read the next handshake Message.
/// This function takes the current state and `handshake_bytes` and returns
/// the next state or a [`TLSError`].
Expand Down Expand Up @@ -165,10 +137,36 @@ val impl_Server__write (self: t_Server) (application_data: Bertie.Tls13utils.t_A
/// The function returns a [`Result`].
/// When successful, the function returns a tuple with the first element the
/// application data as bytes option, and the new [`Server`] state as the second element.
/// If there's no application data, the first element is [`None`].
/// If there\'s no application data, the first element is [`None`].
/// If an error occurs, it returns a [`TLSError`].
val impl_Server__read (self: t_Server) (application_data: Bertie.Tls13utils.t_Bytes)
: Prims.Pure
(Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_AppData & t_Server) u8)
Prims.l_True
(fun _ -> Prims.l_True)

/// Start a new TLS handshake as server.
/// Note that Bertie servers only support a single ciphersuite at a time and
/// do not perform ciphersuite negotiation.
/// This function takes the
/// * `ciphersuite` to use for this server
/// * `db` for the server database containing certificates and keys
/// * `client_hello` for the initial client hello message
/// * `entropy` for the randomness required in the handshake
/// The function returns a [`Result`].
/// When successful, the function returns a three-tuple with the first element the
/// server hello record as bytes, the second the server finished record as bytes,
/// and the new [`Server`] state as the third element.
/// If an error occurs, it returns a [`TLSError`].
val impl_Server__accept
(#iimpl_447424039_: Type0)
{| i1: Rand_core.t_CryptoRng iimpl_447424039_ |}
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(db: Bertie.Server.t_ServerDB)
(client_hello: Bertie.Tls13utils.t_Bytes)
(rng: iimpl_447424039_)
: Prims.Pure
(iimpl_447424039_ &
Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8)
(requires (Bertie.Tls13utils.impl_Bytes__len client_hello <: usize) >=. mk_usize 5)
(fun _ -> Prims.l_True)
Loading
Loading