On Thu, Feb 14, 2013 at 7:19 PM, Luke Wagner <l...@mozilla.com> wrote:
> > Eventually I can imagine writing the JIT in Rust and using some kind of > certified > > compilation to guard against compiler bugs. > > I haven't really followed this topic; do you really think this would be a > feasible approach to a production JS engine? I appreciate that we'd only > have to certify that the jit code was safe, not correct, but that still > doesn't seem significantly easier given the complexity of jit techniques > required to achieve competitive JS performance. > I haven't kept up with the state of the art, but I guess it's feasible with "enough" effort, using a combination of static theorem proving and online verification. For a fully sound system the hardest part might be proving the correctness of GC. It's fair to question whether this is really something we should depend on. On one hand, it's research, on the other hand, technology in this area is improving pretty rapidly. IIRC for Singularity/Midori Microsoft has verified type safety for the entire stack down to the machine code (that's a static compiler, not a JIT, and C#, not JS ... but C# is hard in its own way). I'm more confident that someone will eventually be able to do this than that we'd be able to do it in any given timeframe. > For now, just get it right :-). > > It seems like a scary-large proportion of security sensitive bugs come out > of the JS engine (and it's not because we don't care :). > I thought layout was that scary-large portion :-). > > Sure, the JS JIT will have to be part of the TCB for now. > > If the certified-compilation scheme doesn't work out (this eventuality > seeming rather likely IMHO), it seems like making this TCB assumption early > on would lead us to make some bad architectural decisions that would be > difficult to fix later (a story we know all to well :). > True, but there is also a danger that fear of being architecturally boxed-in causes us to do something over-elaborate :-). I have the impression that the non-JS part of the Web platform grows at a much faster rate than the JS part, and lots of the JS part doesn't even need to be in the TCB. So I hope the proportion of sec-sensitive JS bugs goes down. Maybe. I wonder whether it would make sense to provide process separation and sandboxing in the Rust runtime. Is there any reason why we couldn't identify clusters of Rust tasks and wrap them up into sandboxed processes, verifying message integrity at process boundaries? (Choice of process boundaries would be made manually, I'm not talking about crazy automation.) If that's doable transparently (in semantics, if not performance), sandboxed processes at whatever granularity desired could be retrofitted as needed without changing Servo code. Rob -- Wrfhf pnyyrq gurz gbtrgure naq fnvq, “Lbh xabj gung gur ehyref bs gur Tragvyrf ybeq vg bire gurz, naq gurve uvtu bssvpvnyf rkrepvfr nhgubevgl bire gurz. Abg fb jvgu lbh. Vafgrnq, jubrire jnagf gb orpbzr terng nzbat lbh zhfg or lbhe freinag, naq jubrire jnagf gb or svefg zhfg or lbhe fynir — whfg nf gur Fba bs Zna qvq abg pbzr gb or freirq, ohg gb freir, naq gb tvir uvf yvsr nf n enafbz sbe znal.” [Znggurj 20:25-28] _______________________________________________ dev-servo mailing list dev-servo@lists.mozilla.org https://lists.mozilla.org/listinfo/dev-servo
