The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

More than that, I would be interested to understand what kind of
compromises we are taking when we choose the assumptions we verify
against.
This is particularly relevant for the hardware verification part: what
model of physics gives us the best trade off between verification,
feasability and efficient and reliable HD as a result?

I would not expect the current HD verification systems to take in
account cosmic rays flipping bits...
but may be we should have a statistical verification approach that
takes that into account and verifies a system up to a specific
reliability constraint?

-Similarly... what if there is physical damage (drop the phone on the
floor) or quantum effects....

-For example, the "RowHammer" attack... can it be modelled and verified 
against?


On Sun, 9 Jan 2022 at 08:13, Adam Chlipala <adamc AT csail.mit.edu> wrote:
>
> Thanks for drawing attention to a worthy goal, which I think at least a few 
> different research groups already have in mind, at least philosophically.
>
> For such an effort, setting the goals properly can have a big effect on 
> where it winds up.  I'm not sure it makes sense to ask to "minimize the TCB 
> as much as possible at each step."  Rather, I'd expect that earlier stages 
> are discarded as they are used to produce later stages, and the final stage 
> can be used independently for self-validation.  So, shrinking the TCB in an 
> earlier stage isn't necessarily a good deal, if it delays the completion of 
> later stages.
>
> There are plenty of high-impact proof-assistant developments that never 
> could have been completed so soon if e.g. the original Coq team had decided 
> to wait 20 additional years for the first release, to shrink the TCB as 
> much as they could think up in brainstorming a project roadmap!
>
> Also, I don't think this question has zero practical motivation.  I would 
> hope that, 50 years from now, everyone takes for granted the existence of a 
> repeatable process like you describe, leading to the systems they depend 
> on.  And, even sooner, we should be able to run undergraduate courses that 
> follow such processes toward more modest endpoints.
>
> On 1/8/22 1:41 PM, Talia Ringer wrote:
>
> Something that nerd-sniped me today: Suppose you are building a computer 
> from the ground up, starting with building the hardware. You cannot use any 
> other computers to build or verify anything; this is the only computer in 
> the world, and you have only what you've built at each step. You have no 
> languages, no operating systems, no compilers, no verification tools. All 
> you can do is bootstrap.
>
> Suppose you'd like to verify every single part of the hardware and software 
> stack to the degree possible. It's OK (inevitable I guess) to start with 
> unverified hardware, though, and replace it later with hardware you verify 
> (has anyone done that? It sounds cool). You have two additional goals:
>
> 1) verify as much as possible at each each, and
> 2) minimize the TCB as much as possible at each step.
>
> How would you go about this? What are the biggest conceptual barriers to 
> this, if any? What is the smallest you can get the TCB at any step of the 
> process, and in the end?
>
> This is a purely academic and open-ended question, with zero practical 
> motivation. It just sounds fun to think about and try, and like thinking 
> about it might reveal interesting subproblems that actually have practical 
> motivation.
>
> Talia
>