Looking for 'active' ocap languages (Jessie?) for seL4 research project

[Stewart Webb]

Hi all,

I'm looking into resuming a research project for my Computer Science Masters (@ Melbourne Uni) this year. The initial project when I started it in 2020 was to investigate adopting the Jessie ocap language onto the seL4 microkernel and its capability-based security model (which I have some experience with), to explore whether a better programming model could be produced for using its capability-centric APIs (which in their current C form essentially revert to an ambient authority model). This was all based on a proposal put together by Gernot Heiser at UNSW, one of the core seL4 people.

'Jessie' and Mark Miller's related Javascript-adjacent ocap work (Secure EcmaScript and its various related TC-39 proposals) was the proposed starting point for looking into all of this. However this would probably involve adapting a whole Javascript engine to seL4, which would be doable, but also potentially a lot more work than the scope of one university research project (although it could be argued that making a javascript runtime available for seL4 could be handy for wider adoption... but I digress).

I just spotted another ocap langauge called Pony, which appears to be quite close to C, so that might be better for integrating with seL4 (most of seL4 is written in C and it seems most seL4 programming involves writing C).

My supervisor (who also worked on the original seL4 formal proofs paper) also pointed me in the direction of some early(?) ocap discussion within Rust that could perhaps also be worth looking into? I note a recent post from Alan Karp sharing "A capability-based version of the Rust standard library" https://github.com/bytecodealliance/cap-std, and I believe there has been at least some work done in adapting the Rust toolchain to targeting an seL4 environment.

The original E lang is perhaps another option, but I understand that's Java based and... I don't really want to look into putting Java onto a C-based microkernel either 😅.

Anyhoo thought it would be at least worth asking here for some insights seeing as there seem to be many people here with much more OCap experience than me!

Cheers,

Stewart Webb

[Mark S. Miller]

(Btw, the new name for "Secure EcmaScript" is "Hardened JavaScript".)

Hi Stewart, the others that you mention are also great choices. I know the people involved in Pony and in cap-std, and they're great. They get it and their work is high quality. 

But I'd be especially excited if you did Jessie and/or Hardened JS. As you already know, Jessie is a small subset of Hardened JavaScript. What you may not know, that is directly relevant to the porting effort, is that we're working with Moddable towards a version of their XS JavaScript engine that directly implements Hardened JavaScript. XS is a *small* Hardened JS *interpreter* written in C and built to run on the bare metal of devices, with minimal host-provided C bindings. It makes narrow enough demands of the host that we (Agoric) are running XS as part of our stack on a variety of other hosts, including blockchain.

Of all languages that we've adapted, or seen adapted (including Rust), Hardened JavaScript is unique in the huge amount of existing JavaScript code, not written to run under Hardened JavaScript, that nevertheless does run under Hardened JavaScript securely.

This combination of Hardened JS running, say on XS, running on seL4 would be a dream come true for me. By bridging from language ocaps to OS ocaps, Hardened JS could make the power and security of seL4 adoptable by massive numbers of programmers.

Like Local-E vs (distributed) E, Hardened JS is the local ocap programming language component of Endo https://github.com/endojs/endo , which is our distributed persistent hardened JS. It is how we talk between chain-based computation and off-chain computation, all the way out to the user interface. Would be wonderful for some of the nodes on that network to be running incorruptibly on seL4.

PTAL ;)

[Mark S. Miller]

You should also take a look at Spritely. Another excellent choice, which I'll leave to Christine Webber to explain...

[Raoul Duke]

Do the Jessies and Hardened JSs and XSs additionally support / work
well with some kind of static typing tooling per chance?

[Mark S. Miller]

Yes! TypeScript has defined a set of type checking rules for JS that is unsound but usually intuitive and in widespread use. Most of all, the types are accurate enough to enable the IDE to provide much more useful feedback. However, from a security perspective, the unsoundness is especially challenging. The problem we need to avoid is a programmer reading code with inline type declarations, written as part of the code, believing the type declarations. 

Instead we write in a style we call Proper JS properjs.org , which is that we write all of our code in JS itself, but put typescript declarations in two places: In jsdoc doc-comments, and in declaration-only *.d.ts files. We've configured our tooling so that we get the benefits of the typescript type checker, without mixing in the unreliable type declarations directly into the code. Seeing them in comments suggests exactly the right framing: Like the rest of the comment, it is commentary that is supposed to be about what the code is supposed to be doing. But the comments provide a) no guarantees, and b) have no effect on what happens at runtime.

On Mon, Jan 24, 2022 at 9:10 PM Raoul Duke <rao...@gmail.com> wrote:

Do the Jessies and Hardened JSs and XSs additionally support / work
well with some kind of static typing tooling per chance?

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAJ7XQb4yHSDEOLMqE0AUyZfO%2BPOwSK37OV%3D-hVOp-guSw9CU1w%40mail.gmail.com.

[Stewart Webb]

Thanks for all the info Mark - I had hoped to try get in touch with you directly at some point but wasn't sure if I'd get through with a cold-email...

Thanks especially for the info on this XS JS engine. I'd actually already compiled a list of potential JS engines to investigate wrangling onto seL4:

• duktape
• QuickJS
  
• low.js | Node.js for microcontrollers
• mJS: Restricted JavaScript engine
  

... so I will add XS to this list :). (most of the above examples are also in C)

Something that directly implements SES/Hardened JS at the intepreter/language/engine level seems a lot more desirable - the SES approach of locking down an existing dynamic JS environment with more JS always seemed a bit inelegant to me, but I imagine it was a much easier place to start from.

There's an additional potential issue of any modern JS language features needed to support Jessie... but Babel and/or corejs polyfills might be able to get that kind of thing over the line for at least a proof of concept. Part of the research would no doubt be digging through all of this - I've done a fair bit of ReactJS + Webpack frontend work professionally which may give me a bit of a familiarity leg-up here (and was part of what drew me to the project in the first place).

Are there any samples of code written in Jessie around that I could take a look at as a starting point? I got a bit lost delving through the grammar and QuasiPEG...

And is Jessie itself still in use at Agoric? I seem to remember noting that it had disappeared from the Agoric website, perhaps in favour of 'Zoe' as a smart contract language?

Cheers,

Stewart

[Mike Stay]

The example TypeScript uses on their website to illustrate
unsoundness, function bivariance, is no longer motivating now that
they have dependent types:

https://reperiendi.wordpress.com/2021/01/27/2657/

But they can never fix that because of the amount of legacy code they have.

Here's an article on the sources of unsoundness:
https://effectivetypescript.com/2021/05/06/unsoundness/

> To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD7BoG6WNHSJevXpjWZy0EE%3DjiFcnmtsMF0scCWjW9UUpQ%40mail.gmail.com.



--
Mike Stay - meta...@gmail.com
http://math.ucr.edu/~mike
https://reperiendi.wordpress.com