Metamath Zero paper #7 on Hacker News
102 views
Skip to first unread message
David A. Wheeler
Oct 25, 2019, 4:48:59 PM10/25/19
to metamath
Metamath Zero is #7 on "Hacker News" ( https://news.ycombinator.com/ ), a widely-read aggregator. That's quite impressive. Congrats, Mario!
There's no discussion yet, but if there is it will be at:
https://news.ycombinator.com/item?id=21358674
--- David A. Wheeler
There's no discussion yet, but if there is it will be at:
https://news.ycombinator.com/item?id=21358674
--- David A. Wheeler
Alexander van der Vekens
Oct 26, 2019, 11:42:53 AM10/26/19
to Metamath
.... the numbering is not stable: Metamath Zero is now #46 and will change soon, I assume. The link to the discussion (and there is alrady a discussion meanwhile) will be stable, I hope ...
David A. Wheeler
Oct 26, 2019, 2:31:56 PM10/26/19
to metamath
On Sat, 26 Oct 2019 08:42:53 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> .... the numbering is not stable: Metamath Zero is now #46 and will change
> soon, I assume.
Yes, the Hacker News rankings are intentionally not stable.
> .... the numbering is not stable: Metamath Zero is now #46 and will change
> soon, I assume.
It's designed so that the top 30 items are recent things to look at.
The idea is that people routinely go to the page to see "what's new & interesting".
Getting up to #7 is extraordinarily high.
> The link to the discussion (and there is alrady a
> discussion meanwhile) will be stable, I hope ...
Giovanni Mascellani
Oct 27, 2019, 3:56:33 AM10/27/19
to metamath
Hi,
Il 25/10/19 22:48, David A. Wheeler ha scritto:
upvotes! :-)
I enjoyed reading the paper, and I took the occasion to resume my
attempt of understanding your work on the self verification of MM0.
Yesterday evening, before sleeping, I was wondering whether we will ever
have operating systems that do not enforce any more security boundaries
between processes and between the kernel and the processes and map
everything to the same address space at ring 0, because loading each
process the OS verified a proof that that code would never touch
anything outside its assigned space...
Great work, Mario!
Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles
Il 25/10/19 22:48, David A. Wheeler ha scritto:
> Metamath Zero is #7 on "Hacker News" ( https://news.ycombinator.com/
> ), a widely-read aggregator. That's quite impressive. Congrats,
> Mario!
Yeah, and it's also the first time an HN submission by me goes beyond 10
> ), a widely-read aggregator. That's quite impressive. Congrats,
> Mario!
upvotes! :-)
I enjoyed reading the paper, and I took the occasion to resume my
attempt of understanding your work on the self verification of MM0.
Yesterday evening, before sleeping, I was wondering whether we will ever
have operating systems that do not enforce any more security boundaries
between processes and between the kernel and the processes and map
everything to the same address space at ring 0, because loading each
process the OS verified a proof that that code would never touch
anything outside its assigned space...
Great work, Mario!
Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles
Mario Carneiro
Oct 27, 2019, 5:02:05 AM10/27/19
to metamath
On Sun, Oct 27, 2019 at 3:56 AM Giovanni Mascellani <g.masc...@gmail.com> wrote:
I was wondering whether we will ever
have operating systems that do not enforce any more security boundaries
between processes and between the kernel and the processes and map
everything to the same address space at ring 0, because loading each
process the OS verified a proof that that code would never touch
anything outside its assigned space...
I think there will always be a use for ring 3 (userland). Assuming there are no privilege escalation bugs in the hardware (unlikely, I know), it is the *only* way to run arbitrary code with controlled effects. That is, if I have a block of unknown code and jump into it, anything could happen... except that the hardware guarantees that any ring 0 stuff goes through OS syscalls. In short, it is a hardware sandbox. There is no way to achieve the same result without more overhead or more analysis of the code. (Google's Native Client was an interesting middle ground in this area, where "arbitrary" code is executed but it is first validated that all jumps go inside the program, no illegal instructions appear in the instruction stream, and a few other things so that it can sandbox without a runtime overhead.)
Of course my programme proposes to prove correctness of "all the code", but as long as there is *any* unverified code on the system you have to be able to protect yourself from it, and that means sandboxing.
I mention this briefly in the paper, but that's actually why the verifier is in a separate process; the "small trusted kernel" approach doesn't work unless the language is sufficiently "safe" and restrictive (and verified) that we can prove that "arbitrary" code doesn't trample on the part of the code about which properties of interest are proved (the trusted kernel). If it's in a separate process, then the unverified part of the code can throw whatever tantrums it likes but it won't be able to influence the verified checker without the OS's say-so. (The OS still has to be trusted in this scenario, though.)
Mario
Giovanni Mascellani
Oct 27, 2019, 11:28:08 AM10/27/19
to meta...@googlegroups.com
Il 27/10/19 10:01, Mario Carneiro ha scritto:
ecosystem evolves so that any code is always shipped together with a
proof-of-tameness, that says that that code is going to behave nicely
when you jump in it. So you run your Tor client and download some
program from the worst darknet website, but it comes with a bundled
proof that guarantees that it is going to only access allowed memory
space and only do authorized syscalls through well defined gates
(possibly, provided that there is some way to formalize this in a
trusted way, also that it is not going to take advantage of
microarchitectural attacks like Spectre and co).
Then, since you trust the specification of "being nice" that such
program proved to be conforming to, you happily run it in ring 0. No
worries even if the code is self-modifying: the "being nice"
specification took this into consideration as well (it is probably not a
big problem in the specification; if anything, the additional burden is
put on the prover).
Again, I fully agree that this is an enormous over-engineering: it is
much easier (as we do) to build a processor that enforces privilege
separation. It is just a way to picture in a funny way what extreme
program correctness proving might one day deliver us.
> I mention this briefly in the paper, but that's actually why the
> verifier is in a separate process; the "small trusted kernel" approach
> doesn't work unless the language is sufficiently "safe" and restrictive
> (and verified) that we can prove that "arbitrary" code doesn't trample
> on the part of the code about which properties of interest are proved
> (the trusted kernel). If it's in a separate process, then the unverified
> part of the code can throw whatever tantrums it likes but it won't be
> able to influence the verified checker without the OS's say-so. (The OS
> still has to be trusted in this scenario, though.)
I agree from the viewpoint of MM0. In my scenario the verification would
be made by the kernel before the program is even jumped in the first time.
> Of course my programme proposes to prove correctness of "all the code",
> but as long as there is *any* unverified code on the system you have to
> be able to protect yourself from it, and that means sandboxing.
Yes, my (admittedly, somehow tongue-in-cheek) idea is that the whole
> but as long as there is *any* unverified code on the system you have to
> be able to protect yourself from it, and that means sandboxing.
ecosystem evolves so that any code is always shipped together with a
proof-of-tameness, that says that that code is going to behave nicely
when you jump in it. So you run your Tor client and download some
program from the worst darknet website, but it comes with a bundled
proof that guarantees that it is going to only access allowed memory
space and only do authorized syscalls through well defined gates
(possibly, provided that there is some way to formalize this in a
trusted way, also that it is not going to take advantage of
microarchitectural attacks like Spectre and co).
Then, since you trust the specification of "being nice" that such
program proved to be conforming to, you happily run it in ring 0. No
worries even if the code is self-modifying: the "being nice"
specification took this into consideration as well (it is probably not a
big problem in the specification; if anything, the additional burden is
put on the prover).
Again, I fully agree that this is an enormous over-engineering: it is
much easier (as we do) to build a processor that enforces privilege
separation. It is just a way to picture in a funny way what extreme
program correctness proving might one day deliver us.
> I mention this briefly in the paper, but that's actually why the
> verifier is in a separate process; the "small trusted kernel" approach
> doesn't work unless the language is sufficiently "safe" and restrictive
> (and verified) that we can prove that "arbitrary" code doesn't trample
> on the part of the code about which properties of interest are proved
> (the trusted kernel). If it's in a separate process, then the unverified
> part of the code can throw whatever tantrums it likes but it won't be
> able to influence the verified checker without the OS's say-so. (The OS
> still has to be trusted in this scenario, though.)
be made by the kernel before the program is even jumped in the first time.
Jim Kingdon
Oct 27, 2019, 11:45:50 AM10/27/19
to meta...@googlegroups.com, Giovanni Mascellani
The idea of having code accompanied by a proof of tameness usually goes by the name of "proof carrying code". https://en.m.wikipedia.org/wiki/Proof-carrying_code
vvs
Oct 27, 2019, 12:10:08 PM10/27/19
to Metamath
You might be interested in this: https://en.wikipedia.org/wiki/Singularity_(operating_system)
Mario Carneiro
Oct 27, 2019, 12:20:38 PM10/27/19
to metamath
I think proof-carrying code is most valuable when it comes to things like firmware updates, where the possible damage that can be done is large, but you also can't sandbox the program and you can't afford to watch it do its thing. I wonder if it's possible to have a closed source PCC? o.O I guess it's not much different from the executable itself - you can have a proof without making it any easier to understand what is going on in the program...
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7B64EEE9-C0D0-4988-8C23-7CC3E640A284%40panix.com.
Reply all
Reply to author
Forward
0 new messages