5 ms·

A Fil-C kernel that ran the whole system in the same address space, safely, would sure be something. Getting rid of the overhead of hardware isolation could com

A Fil-C kernel that ran the whole system in the same address space, safely, would sure be something. Getting rid of the overhead of hardware isolation could compensate for some of the overhead of the software safety checks. That was the dream of Microsoft's Singularity project back in the day. I guess there would be no way to verify that precompiled user programs actually enforce the security boundaries. The only way to guarantee safety in such a system would be to compile everything from source yourself.

pizlonator 1y ago
You could have enforcement that binaries use Fil-C rules suing proof carrying code
- kragen 1y ago
  I'm skeptical that PCC can work in practice with existing social practices around software development, because neither users nor implementors can tell the difference between a correct verifier and one that has flaws that aren't being actively exploited yet, but they can sure tell the difference between a fast system and a slow one. The incentives are strong to drive the runtime cost as close to zero as possible, which involves making your proof-checking system so expressive that it's hard to get right. The closer you get to zero, the more performance-sensitive your userbase gets. No part of your userbase is actively testing the parts of your verifier that reject programs; they try to avoid generating programs that get rejected, and as the verifier gets larger and larger, it requires more and more effort to generate code that exploits one of its bugs, although there are more and more of them. As the effort required to slip malicious code past the verifier grows, the secret in-house tools developed by attackers gives them a larger and larger advantage over the defenders. Continued "maintenance" applied to the verifier drive its size and complexity up over time, driving the probability of a flaw inexorably toward 100%, while, if it is not "maintained" through continuous changes, it will break as its dependencies change, it will be considered outdated, and nobody will understand it well enough to fix a bug if it does surface. We've seen this happen with Java, and although it's clearly not unavoidable in any kind of logical sense, it's a strong set of social pressures. Dynamic checking seems much more memetically fit: developers will regularly write code that should fail the dynamic checks, and, if it passes instead, they will send you an annoyed bug report about how they had to spend their weekend debugging.
  - zozbot234 1y ago
    Proof carrying code is efficient at runtime; the verifier only ever has to run once to verify the binary, which in principle can simply be done at install. Even the verification itself can be fast enough because it's only checking the soundness of existing proofs, not having to generate new ones from scratch. Where there are genuine needs to "make the proof system more expressive", this can be done by adding trusted axioms which will generally be simple enough to manually check; the verifier itself need not become more complex. We've seen a lot of complexity happen with Java but that was generally in the standard library facilities that are bundled with the language and runtime, not really the basic JVM type checking pass. Proof carrying code is closer to the latter.
    - kragen 1y ago
      I agree that the verifier performance is not important to runtime performance (though there have been some changes to the JVM in particular to speed up class loading), but the expressivity of the safety proofs it can check is, because safety properties that cannot be proven at load time must be checked at runtime. Initially, and I think still, the JVM's downcast on loading an object reference from a generic container like ArrayList<Price> is an example: javac has proven statically that it is safe, but the JVM bytecode cannot express that. Pointer nullability in JVM languages like Kotlin is another example: Kotlin knows most object pointers can't be null, but the JVM still has to check at runtime. There have been numerous holes discovered in various implementations of the basic JVM type checking, often after existing for many years.
      - pizlonator 1y ago
        The JVM byte code situation isn’t a great example because that was a series of deliberate design choices for lots of complex reasons. And, the JVM absolutely can guarantee memory safety at the bytecode level. It’s just working with a slightly more dynamic type system than Java source. What would happen if you tried to do PCC for InvisiCaps and FUGC is that it would ultimately constrain what optimizations are possible, because the optimizer would only be able to pick from the set of tricks that it could express a proof for within whatever proof system we picked Totally not the end of the world. Do I think this an interesting thing to actually do? I’m not sure. It’s certainly not the most interesting thing to do with Fil-C right now
miki123211 1y ago
This is what IBM I[1] (AKA AS400) does I think. Ibm I applications are compiled to a hardware-independent intermediate representation called TIMI, which the SLIC (kernel) can then compile down to machine code, usually at program installation time. As the SLIC is also responsible for maintaining system security, there's no way for a malicious user to sneak in a noncompliant program. [1] https://en.wikipedia.org/wiki/IBM_i https://en.wikipedia.org/wiki/IBM_i
- ptx 1y ago
  That's basically the same idea as WebAssembly, isn't it?
  - zozbot234 1y ago
    I don't think WebAssembly has been applied across a whole system just yet. Inferno/Limbo (the successor to Plan9, using the Dis virtual machine) may be substantially closer to the mark, along with AOSP (based on Dalvik/ART) and a variety of JavaScript-based "web" OS's. One may also argue that "image"-based systems like Smalltalk, Oberon etc. are in the same class, and that the lineage ultimately originates from Lisp machines.
    - kragen 1y ago
      Smalltalk predates Lisp machines and didn't originally compile to native code at all. I don't remember if Limbo did. Oberon isn't image-based (you can't save and restore the memory state of the running system) and didn't originally define a machine-independent bytecode format, and the one it had for many years has been removed from the current version. Wasm usually isn't image-based either; though it has a clear pathway for doing so, for example Wasmtime still doesn't implement that functionality: https://github.com/bytecodealliance/wasmtime/issues/3017 https://github.com/bytecodealliance/wasmtime/issues/3017
      - miki123211 1y ago
        AS400 isn't image based either. And unlike AS400, I don't think either Smalltalk or Lisp machines used the bytecode abstraction to achieve security.

pizlonator 1y ago

You could have enforcement that binaries use Fil-C rules suing proof carrying code

kragen 1y ago
I'm skeptical that PCC can work in practice with existing social practices around software development, because neither users nor implementors can tell the difference between a correct verifier and one that has flaws that aren't being actively exploited yet, but they can sure tell the difference between a fast system and a slow one. The incentives are strong to drive the runtime cost as close to zero as possible, which involves making your proof-checking system so expressive that it's hard to get right. The closer you get to zero, the more performance-sensitive your userbase gets. No part of your userbase is actively testing the parts of your verifier that reject programs; they try to avoid generating programs that get rejected, and as the verifier gets larger and larger, it requires more and more effort to generate code that exploits one of its bugs, although there are more and more of them. As the effort required to slip malicious code past the verifier grows, the secret in-house tools developed by attackers gives them a larger and larger advantage over the defenders. Continued "maintenance" applied to the verifier drive its size and complexity up over time, driving the probability of a flaw inexorably toward 100%, while, if it is not "maintained" through continuous changes, it will break as its dependencies change, it will be considered outdated, and nobody will understand it well enough to fix a bug if it does surface. We've seen this happen with Java, and although it's clearly not unavoidable in any kind of logical sense, it's a strong set of social pressures. Dynamic checking seems much more memetically fit: developers will regularly write code that should fail the dynamic checks, and, if it passes instead, they will send you an annoyed bug report about how they had to spend their weekend debugging.
- zozbot234 1y ago
  Proof carrying code is efficient at runtime; the verifier only ever has to run once to verify the binary, which in principle can simply be done at install. Even the verification itself can be fast enough because it's only checking the soundness of existing proofs, not having to generate new ones from scratch. Where there are genuine needs to "make the proof system more expressive", this can be done by adding trusted axioms which will generally be simple enough to manually check; the verifier itself need not become more complex. We've seen a lot of complexity happen with Java but that was generally in the standard library facilities that are bundled with the language and runtime, not really the basic JVM type checking pass. Proof carrying code is closer to the latter.
  - kragen 1y ago
    I agree that the verifier performance is not important to runtime performance (though there have been some changes to the JVM in particular to speed up class loading), but the expressivity of the safety proofs it can check is, because safety properties that cannot be proven at load time must be checked at runtime. Initially, and I think still, the JVM's downcast on loading an object reference from a generic container like ArrayList<Price> is an example: javac has proven statically that it is safe, but the JVM bytecode cannot express that. Pointer nullability in JVM languages like Kotlin is another example: Kotlin knows most object pointers can't be null, but the JVM still has to check at runtime. There have been numerous holes discovered in various implementations of the basic JVM type checking, often after existing for many years.
    - pizlonator 1y ago
      The JVM byte code situation isn’t a great example because that was a series of deliberate design choices for lots of complex reasons. And, the JVM absolutely can guarantee memory safety at the bytecode level. It’s just working with a slightly more dynamic type system than Java source. What would happen if you tried to do PCC for InvisiCaps and FUGC is that it would ultimately constrain what optimizations are possible, because the optimizer would only be able to pick from the set of tricks that it could express a proof for within whatever proof system we picked Totally not the end of the world. Do I think this an interesting thing to actually do? I’m not sure. It’s certainly not the most interesting thing to do with Fil-C right now

miki123211 1y ago

This is what IBM I[1] (AKA AS400) does I think. Ibm I applications are compiled to a hardware-independent intermediate representation called TIMI, which the SLIC (kernel) can then compile down to machine code, usually at program installation time. As the SLIC is also responsible for maintaining system security, there's no way for a malicious user to sneak in a noncompliant program. [1] https://en.wikipedia.org/wiki/IBM_i https://en.wikipedia.org/wiki/IBM_i

ptx 1y ago
That's basically the same idea as WebAssembly, isn't it?
- zozbot234 1y ago
  I don't think WebAssembly has been applied across a whole system just yet. Inferno/Limbo (the successor to Plan9, using the Dis virtual machine) may be substantially closer to the mark, along with AOSP (based on Dalvik/ART) and a variety of JavaScript-based "web" OS's. One may also argue that "image"-based systems like Smalltalk, Oberon etc. are in the same class, and that the lineage ultimately originates from Lisp machines.
  - kragen 1y ago
    Smalltalk predates Lisp machines and didn't originally compile to native code at all. I don't remember if Limbo did. Oberon isn't image-based (you can't save and restore the memory state of the running system) and didn't originally define a machine-independent bytecode format, and the one it had for many years has been removed from the current version. Wasm usually isn't image-based either; though it has a clear pathway for doing so, for example Wasmtime still doesn't implement that functionality: https://github.com/bytecodealliance/wasmtime/issues/3017 https://github.com/bytecodealliance/wasmtime/issues/3017
    - miki123211 1y ago
      AS400 isn't image based either. And unlike AS400, I don't think either Smalltalk or Lisp machines used the bytecode abstraction to achieve security.