fuklief

It's better to use a constant time algorithm, but that's harder to do in a curve generic way and has a pretty significant performance impact (particular before the safegcd paper).

Crypto noob here, but isn't modular inverse the same as modular exponentiation through Fermat's little theorem? I.e., x^-1 mod n is the same as computing x^{n - 2} mod n which we know how to do in a constant-time way with a Montgomery ladder. Or is that too slow?

I didn't know US/UK gov were against hybrids. AFAIU, the French and Germans are recommending hybrids as a first step before stand alone PQC [0].

[0] https://cyber.gouv.fr/en/publications/follow-position-paper-...

This survey by the same author also provides a good comparison https://saaramar.github.io/memory_safety_blogpost_2022/

I believe it means flattening the AST, here is a nice blog post about this technique https://www.cs.cornell.edu/~asampson/blog/flattening.html

I personally did not know about classes prépa before the last year of high school. I will forever be thankful for my maths teacher who told me about it that year, since I would have probably slacked off at university.

- Make them good at science, i.e., Maths and Physics.

- Get them into a decent high school, e.g., Henri 4 or Louis Le Grand in Paris.

- Hope they have good grades and manage to get into a good preparatory class [1], e.g., Henri 4, Louis Le Grand in Paris, or Hoche and Sainte-Geneniève in Versailles.

- Make sure they don't slack off, and hope they get into a good engineer school, e.g., Ecole Polytechnique, Ecole des Mines, Ecole Nationale des Ponts et Chaussés, CentraleSupelec.

(Lists are not exhaustive)

If they manage to get into one of these schools, they will most likely end up not have any difficulty to find a somewhat well-paid job in France.

[1] https://en.wikipedia.org/wiki/Classe_pr%C3%A9paratoire_aux_g...

Maybe they thought it's spelled "your" instead of "you're".

Google put in significant engineering effort into "Ryu", a parsing library for double-precision floating point numbers: https://github.com/ulfjack/ryu

It's not a parsing library, but a printing one, i.e., double -> string. https://github.com/fastfloat/fast_float is a parsing library, i.e., string -> double, not by Google though, but was indeed motivated by parsing JSON fast https://lemire.me/blog/2020/03/10/fast-float-parsing-in-prac...

See CHERI and Arm Morello https://www.arm.com/blogs/blueprint/morello

Probably was some dude’s L7 promo project in AWS.

Actually a former CS prof at Maryland moving to industry. https://mhicks.me/

In other words, CHERI can reduce memory-unsafety related slowdowns by two thirds, which is pretty incredible. AMD CPUs are even starting to have hardware support for it, bringing its run-time overhead down to 6.8%.

Source on AMD CPUs having support for CHERI-style capabilities ? Afaik, there is only the Arm Morello prototype out right now and FPGAs.

I believe it means High Level Synthesis in this context.

You might be interested in [Catala](https://catala-lang.org/en/), a domain specific language for implementing legislative texts. Iirc, they have worked on the french tax code, and are starting on the us one now.

I'm using the following for fonts.

  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
  \usepackage[largesc]{newpxtext}
  \usepackage{newpxmath}
  \usepackage[supsfam=newpx]{superiors}

Would virtual memory still be necessary on a capability machine architecture [0] ? My understanding is that would not be the case since all programs can only access memory that's been allocated to it. By definition, capabilities cannot be created out of thin air like pointers can be ?

[0] https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/

By "register allocation verifier", I meant the checker as mentioned in the post you quote.

In CompCert's case though, the register allocation verifier itself is verified. I'm not so sure the SMT solver used here are.

Word on the block is that there is a RFC to add support for secret types in LLVM, and Rust is waiting for them to also provide it in Rust [0].

[0] https://github.com/rust-lang/rfcs/pull/2859

... leakage by timing side-channels depends in parts on how accurate your time-measurements are (e.g. Javascript's timer resolution was degraded, in order to make transient failure attacks like Spectre harder [1]).

But that doesn't matter if how long it takes for your instructions to execute is data independent, no ?

So what kind of formal verification is it ? Is it proof assistant, model checking ? And what does it verify ? It's not really clear from a first glance.

That sounds like a capability machine e.g., CHERI[1] It seems those might become relatively mainstream in a few years, as ARM seems to be jumping on board [2]

[1] https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ [2]: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...

If you pay for spotify, https://www.jqbx.fm/ can do that.

Credit card = Débit différé in France (aka. you pay for everything at the end of the month), it's even written Credit on the card.

And most online banks (e.g., Boursorama, Hello Bank, Fortuneo, etc) do not charge you a monthly fee for a card.

+1

What does it even mean that the language is formally provable ?!

CertiKOS is verified in Coq, I don't see why you say it isn't fit to get work done.

Currently, yes. Eventually, no.

Meanwhile, Google researchers (Plotkin and Abadi) are going to present "A Simple Differentiable Programming Language" at POPL20[1] in January.

I can't find a preprint though :'(

[1] https://popl20.sigplan.org/track/POPL-2020-Research-Papers#e...

I'm guessing at least the sponsors of the OCaml software foundation: https://ocaml-sf.org/sponsors/

Does it have to be tech related ? What if I want to make a small group to meet people for boardgames or something ?

CompCert ?