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