Hacker News Reader

fukliefon Who's afraid of a big bad optimizing compiler?

CompCert ?

fukliefon Fatal Dose – Radiation Deaths linked to AECL Computer Errors (1994)

In my field, we use this kind of example to tell people that testing sucks or is not enough and that we need to formally/mathematically prove that software is free of bugs for critical systems.

fukliefon A Mechanised Cryptographic Proof of the WireGuard VPN Protocol

The abstract says cryptoverif is a proof assistant, but the cryptoverif page says it's an automatic protocol prover.

Which is it ? (my understanding is that a proof assistant is interactive, like Coq, Agda, etc)

fukliefon EverCrypt, a cryptographic library that is provably secure against known attacks

> The mathematical proof might be 100% solid and hacker proof. The implementation will probably never be.

I agree, I see a few ways that it could go wrong:

- Code is proven correct against the specification, but specification is wrong/buggy

- source code is correct/secure, but compiler is overzealous and botch the securities guarantees.

fukliefon Formally Verified Software in the Real World (2018)

Are you sure on that? It was B method they used afaik.

fukliefon CompCert – A formally verified C compiler

Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ?

fukliefon Ask HN: Where to go for the cheapest EE degree in the U.S.? In the World?

It's more around 1300 euros actually :-) And it's only possible for EU citizens afaik.

fukliefon Tezos and Ocaml: A self-amending cryptographic ledger

Considering the close ties of OCaml and Coq, has anyone done some sort of formal verification for Tezos ?

fukliefon Checked C: extension to C that adds static and dynamic checking

How does it compare to CCured ?

fukliefon Show HN: A HN/Reddit-style site for scientific pre-prints and publications

Some idea for other subs: Computer Science/Maths/Physics should be the most common I think

Also https://eprint.iacr.org/ is used a lot for publishing crypto preprints

fukliefon Show HN: A HN/Reddit-style site for scientific pre-prints and publications

It seems really skewed towards biology publications, is it on purpose ?

fukliefon Why Constant-Time Crypto?

"Instead I'd produce a restricted C compiler that only accepted constant time programs, and mapped directly to a limited set of machine instructions."

How would the compiler knows if the code it's given is constant-time ? It's actually a property quite hard to verify due to pointer aliasing or whatnot.

Another angle is to have a compiler that always outputs constant-time code. It's always possible, at least for crypto code according to Peter Schwabe, just that it's probably not going to be very fast code...

fukliefon The C standard formalized in Coq

Coq is also used in industry, in particular by Airbus with the CompCert C compiler.

fukliefon C to Java Translation. Automatic, Complete, Correct. Free for Open-Source.

It says the translation is correct, is there any proof of that ?