<div dir="ltr"><br><br><div class="gmail_quote"><div dir="ltr">On Sat, Oct 6, 2018 at 11:03 PM Barak A. Pearlmutter <<a href="mailto:barak@pearlmutter.net">barak@pearlmutter.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">At a high level, you seem to be proposing encoding and enforcing<br>
safety properties of executables using a type system. One<br>
instantiation of this idea is proof-carrying-code (Necula and Lee,<br>
1996, see <a href="https://en.wikipedia.org/wiki/Proof-carrying_code" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Proof-carrying_code</a>), which<br>
ensures safety properties of machine code. </blockquote><div><br></div><div>I would guess a factor that prevented something like PCC from taking off is the fact that proofs over binaries are relatively pretty challenging to express and verify, and ISA semantics tend to be really complicated.</div><div><br></div><div>I think an intermediate approach that might be a lot cheaper to implement is to ship some sort of IR (rather than machine code) that is A) relatively cheap to check and compile and B) carries some variety of safety guarantee.</div><div><br></div><div>As I recall, A) is already in use. Apple requires developers to submit applications as LLVM IR rather than machine code.</div><div><br></div><div>LLVM IR definitely isn't designed with B) in mind, however. I could imagine something like Core being useful here. A fully annotated type-checked language with semantics amenable to formal analysis.</div><div><br></div><div>You could add some sort of effects system to the type system of the IR, as a basis for enforcing security policies. E.g. network access could be an effect.</div><div><br></div><div>The advantage of doing this over PCC is that we don't have to retrofit the proof system to match the ISA, but instead can design the IR specifically to make the proof system easy. A downside is that you have to compile the application once upon downloading it, but this doesn't seem to cause too much of an issue in practice.</div><div><br></div><div><br></div><div>  </div></div></div>