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

Panic freedom with F* #133

Draft
wants to merge 12 commits into
base: main
Choose a base branch
from
Draft

Panic freedom with F* #133

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 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
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
6 changes: 2 additions & 4 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,17 +21,15 @@ libcrux-kem = { git = "https://github.com/cryspen/libcrux", features = ["kyber"]
libcrux = { git = "https://github.com/cryspen/libcrux", features = [
"rand",
]}
hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
hax-lib = { git = "https://github.com/hacspec/hax" }
hax-lib = { git = "https://github.com/hacspec/hax/", branch= "pq11-fstar-libs" }
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's remember to update this before merging.



[features]
default = ["api", "std"]
std = []
test_utils = []
secret_integers = []
api = [] # The streaming Rust API that everyone should use but is not hacspec.
hax-fstar = ["dep:hax-lib-macros"]
hax-pv = ["dep:hax-lib-macros"]

[dev-dependencies]
bertie = { path = ".", features = ["test_utils"] }
Expand Down
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 @@ -97,7 +97,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
47 changes: 41 additions & 6 deletions proofs/fstar/extraction/Bertie.Server.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,35 @@ module Bertie.Server
open Core
open FStar.Mul

let _ =
(* This module has implicit dependencies, here we make them explicit. *)
(* The implicit dependencies arise from typeclasses instances. *)
let open Bertie.Tls13utils in
()

let impl__ServerDB__new
(server_name cert sk: Bertie.Tls13utils.t_Bytes)
(psk_opt: Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
= { f_server_name = server_name; f_cert = cert; f_sk = sk; f_psk_opt = psk_opt } <: t_ServerDB

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_1': Core.Fmt.t_Debug t_ServerDB

let impl_1 = impl_1'

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_2': Core.Clone.t_Clone t_ServerDB

let impl_2 = impl_2'

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_3': Core.Default.t_Default t_ServerDB

let impl_3 = impl_3'

let lookup_db
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(db: t_ServerDB)
Expand All @@ -25,15 +49,22 @@ let lookup_db
Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
with
| true, Core.Option.Option_Some ctkt, Core.Option.Option_Some (stkt, psk) ->
(match Bertie.Tls13utils.check_eq ctkt stkt with
(match Bertie.Tls13utils.check_eq ctkt stkt <: Core.Result.t_Result Prims.unit u8 with
| Core.Result.Result_Ok _ ->
let server:t_ServerInfo =
{
f_cert = Core.Clone.f_clone db.f_cert;
f_sk = Core.Clone.f_clone db.f_sk;
f_cert
=
Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes
#FStar.Tactics.Typeclasses.solve
db.f_cert;
f_sk
=
Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve db.f_sk;
f_psk_opt
=
Core.Option.Option_Some (Core.Clone.f_clone psk)
Core.Option.Option_Some
(Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve psk)
<:
Core.Option.t_Option Bertie.Tls13utils.t_Bytes
}
Expand All @@ -46,8 +77,12 @@ let lookup_db
| false, _, _ ->
let server:t_ServerInfo =
{
f_cert = Core.Clone.f_clone db.f_cert;
f_sk = Core.Clone.f_clone db.f_sk;
f_cert
=
Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve db.f_cert;
f_sk
=
Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve db.f_sk;
f_psk_opt = Core.Option.Option_None <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes
}
<:
Expand Down
21 changes: 21 additions & 0 deletions proofs/fstar/extraction/Bertie.Server.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,24 +3,45 @@ module Bertie.Server
open Core
open FStar.Mul

let _ =
(* This module has implicit dependencies, here we make them explicit. *)
(* The implicit dependencies arise from typeclasses instances. *)
let open Bertie.Tls13utils in
()

/// The Server Database
type t_ServerDB = {
f_server_name:Bertie.Tls13utils.t_Bytes;
f_cert:Bertie.Tls13utils.t_Bytes;
f_sk:Bertie.Tls13utils.t_Bytes;
f_psk_opt:Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes)
}

/// Create a new server database.
/// Note that this only holds one value at a time right now. #51
val impl__ServerDB__new
(server_name cert sk: Bertie.Tls13utils.t_Bytes)
(psk_opt: Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
: Prims.Pure t_ServerDB Prims.l_True (fun _ -> Prims.l_True)

/// Global server information.
type t_ServerInfo = {
f_cert:Bertie.Tls13utils.t_Bytes;
f_sk:Bertie.Tls13utils.t_Bytes;
f_psk_opt:Core.Option.t_Option Bertie.Tls13utils.t_Bytes
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_1:Core.Fmt.t_Debug t_ServerDB

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_2:Core.Clone.t_Clone t_ServerDB

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_3:Core.Default.t_Default t_ServerDB

/// Look up a server for the given `ciphersuite`.
/// The function returns a server with the first algorithm it finds.
val lookup_db
(ciphersuite: Bertie.Tls13crypto.t_Algorithms)
(db: t_ServerDB)
Expand Down
Loading
Loading