[HN Gopher] Bertie - A minimal, high-assurance implementation of...
___________________________________________________________________
Bertie - A minimal, high-assurance implementation of TLS 1.3
written in hacspec
Author : g0xA52A2A
Score : 105 points
Date : 2024-03-23 12:12 UTC (10 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| thulle wrote:
| I see hacspec using secret-integers: "wrapper around integer
| types for constant-timedness". Does Hacspec/Bertie have
| assurances about constant-timedness too?
| manfre wrote:
| 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.
| dudus wrote:
| 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 wrote:
| Sounds like SPARK Ada and Frama-C.
| mdaniel wrote:
| 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 wrote:
| > _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.)
| csande17 wrote:
| 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.
| necubi wrote:
| 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 wrote:
| Besides aiding in verification, does writing an austere TLS
| implementation like this also potentially make it suitable for
| resource-constrained targets, like microcontrollers?
| eptcyka wrote:
| If it has an FFI, it'll definitely beat compiling openssl
| wherever you can get by with just using tls1.3.
___________________________________________________________________
(page generated 2024-03-23 23:00 UTC)