Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec | Hacker News Reader

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

github.com

135 pointsg0xA52A2A13 comments

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

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

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

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.

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.

Sounds like SPARK Ada and Frama-C.

> 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?

I do find myself painstakingly repeating tests after every commit no matter how minor it is.

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?

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...

> 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.)

Well, the Apache License does say "You must give any other recipients of the Work or Derivative Works a copy of this License" when you're redistributing the code. Including a copy of the license in the repo makes it easier for people to comply with that requirement.

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.

Reply on news.ycombinator.com