Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec

by g0xA52A2A • 2 years ago

135 13 2 years ago

thulle• 2 years ago

I see hacspec using secret-integers: "wrapper around integer types for constant-timedness". Does Hacspec/Bertie have assurances about constant-timedness too?

manfre• 2 years ago

hacspec

This is the successor of https://github.com/HACS-workshop/hacspec but a predecessor of https://github.com/hacspec/hax. Development in this repository has mostly stopped, see hax instead.

dudus2• 2 years ago

I don't think it matters because hacspec on this case is just the language which is a subset of rust. He still just uses cargo so treat it as rust code.

The point is that you can check the binary against some sort of formal definition to make sure the implementation you have at hand has not been tampered with. But it seems the idea is to check during dev not usage which for me is a missed opportunity. Why can't it check if it's correct every time it's loaded?

   Keep in mind that Bertie is written in hacspec -- a more "restrictive" version of Rust that lends itself to formal verification. Working on Bertie feels a lot like working on a typical Rust crate but all code needs to be valid according to hacspec. Thus, you may also find that some code is "unusual" compared to vanilla Rust.

nickpsecurity• 2 years ago

Sounds like SPARK Ada and Frama-C.

tialaramex• 2 years ago

Why can't it check if it's correct every time it's loaded?

This is considerable extra work and it's pointless. When you add together some numbers do you find yourself having to painstakingly re-assess whether the Peano Axioms (which make arithmetic work) do what you expected for the numbers you're adding? But what if today, this time, 2 + 2 is 7 or 5 instead of 4?

rfl890• 2 years ago

At runtime you could simply verify the dll‘s signature or any other generic code integrity solution? Why go to all the trouble to verify your implementation at runtime when you could do it at compile time?

mdaniel• 2 years ago

I have no idea what the legal weight is for a toml field so this repo really would benefit from having a formal copy of the Apache-2 license file https://github.com/hacspec/hax/blob/2da100068e9ae5e69e5b35bb... similar to its MIT friend https://github.com/hacspec/hacspec/blob/4ecc847fc944fe996e19...

wizzwizz4• 2 years ago

I have no idea what the legal weight is for a toml field

Law is usually about what's communicated. If "Apache-2" unambiguously refers to a particular license, I don't see the benefit in including a copy of it. (I'd go for "Apache-2.0", though – as they've done –, since that's the SPDX short identifier.)

necubi• 2 years ago

My understanding is that hacspec is the language (a subset of rust), and hax is the tool that compiles it into format proof languages like Coq. Some explanation of the name changes here: https://hacspec.org/blog/posts/hax-v0-1/

A group of us started hacspec (high assurance crypto specifications), a language for specifying cryptographic primitives as the basis for formal verification, in early 2018 at the HACS workshop. After two iterations on hacspec the project outgrew the name and the initial crypto-oriented scope.
Here comes hax. hax is a tool for high assurance translations that translates a large-ish subset of safe Rust into the formal languages accepted by proof assistants such as F* or Coq. Backends for other provers like EasyCrypt are under construction.

skibz• 2 years ago

Besides aiding in verification, does writing an austere TLS implementation like this also potentially make it suitable for resource-constrained targets, like microcontrollers?

eptcyka• 2 years ago

If it has an FFI, it'll definitely beat compiling openssl wherever you can get by with just using tls1.3.

Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec

Related Stories