hannesm

What you already can do is attaching gdb -- either live or at a core dump. Please see https://github.com/Solo5/solo5/blob/master/docs/debugging.md for detailed instructions ;)

What you as well can do is record-replay -- well, at least there used to be this option, I'm now lost whether it has never been merged anywhere, or it is stuck in some PR somewhere. This was truly great - since the external interface is so thin, it is easily doable to dump all external events (API calls and returns) onto disk and replay one-by-one, inspecting the state.

To be a bit more precise, what we achieved so far: apart from web servers and TLS reverse proxies (with DNS-backed let's encrypt provisioning), DNS authoritative servers, a CalDAV server, git client and servers, SMTP stack (including dkim etc.), OpenVPN implementation, archive mirror (using tar as file system), monitoring with syslog and influx, ...

A big milestone was binary releases and deployment instructions, see https://robur.coop/Projects/Reproducible_builds

see more at https://blog.robur.coop https://hannes.robur.coop https://blog.osau.re/ https://reyn.ir/archive.html

If you're curious how/what to integrate MirageOS into your infrastructure, please reach out (best via email).

good news is that MirageOS can as well be executed in a seccomp context with only 5 or 7 system calls allowed -- see the spt target of solo5 https://github.com/solo5/solo5 -- also this great talk by mato https://archive.fosdem.org/2019/schedule/event/solo5_unikern...

Some MirageOS developers were hired/acquired by docker -- though not the (open source) project, beither the code... There's still quite some work on MirageOS itself, including reproducible binary builds, VPN, DNS services, orchestration solutions, ...

Amazing how little code is needed for that, and how clear the interface is... documentation and tutorials at https://docs.osau.re/miou/

srsly it's 2022 and they only have legacy IP and no IPv6?

Yes, this is an ordinary Linux binary.

The attack surface is different, you may be interested in https://archive.fosdem.org/2019/schedule/event/solo5_unikern... and/or https://archive.fosdem.org/2019/schedule/event/solo5_unikern... :)

TL;DR: hardware virtualization is pushing trust into hardware -- but can you trust the hardware implementation (to isolate memory)?

MirageOS is - similar to the latest OCaml release - only using a single CPU core. You can run multiple unikernels, one on each core. If doing that, you can use Xen vchan (shared memory), or TCP for marshalling.

> Also I would say there are reasons for isolation beyond memory safety.

Would you mind to elaborate which reasons you are thinking of?

Maybe https://hannes.robur.coop/Posts/Monitoring sheds some light how to monitor MirageOS unikernels ;)

We use asynchronous tasks in MirageOS (cooperative multitasking) using lwt http://ocsigen.org/lwt/latest/manual/manual, so you can serve multiple network connections at the same time.

Since there are no processes, there's no concept of "fork", but indeed you can run multiple tasks at the same time (using the same address space). Why again would you need multiple processes? Since the programming language OCaml has a semantics and is memory-safe, there's no strong reason for isolation at execution time (apart from the C bits, which we try to keep to a minimum and compile with runtime safety flags (red-zone for stack protection, mapping execute-only (seems to only reliably work on OpenBSD), etc.)).

In ancient times, only Xen was supported. Nowadays, the support moved to:

  - Xen (PVH)
  - Linux KVM, FreeBSD BHyve, OpenBSD VMM
  - SPT (seccomp, no hardware virtualization)
  - virtio (GCE, ..)
  - muen (muen.sk)

Take a look at https://github.com/solo5/solo5 which is used as the low level bits to run OCaml.

Highly recommend the history of English podcast, which goes deep into the topics https://historyofenglishpodcast.com/

Processes? Seriously if there's only a single one, why would you waste resources on process management and process information? Just get over it ;) http://unikernel.org https://mirage.io :D

Looks like we're on a different Interweb, works for me; and travis was a spurious reporting problem, compiles fine (and is now green just to make you happy) :)

There's https://nqsb.io - now even with a libtls.so compat layer (you can LD_PRELOAD our libnqsb-tls https://github.com/mirleft/libnqsb-tls)

Being binary compatible with libssl.so is just insane (too many symbols), but obviously doable. Volunteers welcome

Have you seen unikernel approaches like MirageOS (https://mirage.io), which challenge the POSIX basics of operating systems? If not, take a look :)

This is similar to my experience verifying imperative code (as part of http://itu.dk/research/tomeso): rewrite code as pure as possible (learning that mutation is premature optimisation), then try to specify and prove it.

Aside, if we're reinventing the wheel anyways, why not in a proper style? There's no reason to not deploy purely functional code (+some effectful shims). Think https://mirage.io https://nqsb.io -- rust has way too much mutation and unsafe builtin already...

hmm, my other OS is MirageOS (https://mirage.io) -- also see https://nqsb.io contains my previous two years of work ;)

I'd rather call it extensive exploration than fuzz testing what is in my mind...

The specification, as written in the RFC, is pretty useless... But luckily people sat down and formalised TCP/IP as spoken on the Internet (10 years ago, Linux-2.4.20/FreeBSD-4.6/Windows XP): https://www.cl.cam.ac.uk/~pes20/Netsem/index.html

All the code is now BSD licensed https://github.com/PeterSewell/netsem

What is missing in 10 years of TCP? Apart from SACK and delayed ACK not much it seems (in FreeBSD congestion control algorithms are pluggable nowadays).

And I currently revive it (working hard on test suite using DTrace probes) https://www.cl.cam.ac.uk/~pes20/HuginnTCP/

Please ping me if you're interested (hannes at mehnert dot org) and eager to help.

You have seen the network semantics research project https://www.cl.cam.ac.uk/~pes20/Netsem/index.html? It is a formal model of TCP/IP validated with Linnux 2.4.20/FreeBSD-4.6/Windows XP (yes, that was ~10 years ago).

It is nowadays BSD licensed on GitHub https://github.com/PeterSewell/netsem (and I'm currently reviving it https://www.cl.cam.ac.uk/~pes20/HuginnTCP/)...

it is btw roughly http://nonwhiteheterosexualmalelicense.org/

why not then print a shared secret on your business card, and use the socialist millionaires problem (https://en.wikipedia.org/wiki/Socialist_millionaire)?

edited, added some explanation: (since there's a time span between handing out your card and verifying the FP, in which your key might have get compromised... and thus the one who received the card cannot verify whether you really got compromised and needed to update your key, or an attacker intercepted with a new key)...

[author of jackline here] interesting idea, but since I'm not willing to audit all the other xmpp clients, I won't import any OTR private keys. I'm willing to import trusted fingerprints of contacts, though.

also, imho people should get used to key rollover / revocation / renewals, rather than pretending that you have a life-long key.

some might have heard of this TLS stack as OCaml-TLS, but we rebranded it for our Usenix security paper. The paper includes an evaluation of common vulnerabilities in widely used TLS stacks in 2014.

this is impressive, and you can even first compile the unikernel as unix binary and run the webserver standalone, before deploying your virtual machine to your hosting provider!

it's in progress of getting deployed (https://travis-ci.org/mirage/mirage-www/builds/68516629) -- raw source of the security page at https://github.com/mirage/mirage-www/blob/master/tmpl/securi...

A name, once taken, cannot be unclaimed. If the package should be removed, an empty delegation will be put there.

It is not clear to me what you are reading in the proposal. There is no need for DNS and SSL hosting. Packages are put as tarball onto the Internet. Then in the opam-repository the metadata, including a signature over the tarball. The tarball is fetched (over any insecure connection) and its signature is verified. The naming and trust delegation happens within opam and the opam repository.

How is an update supposed to work if the connection to the timestamp is prevented/intercepted? How if the connection to the repository is prevented/intercepted? Using a single connection leads to less potential failure modes.

I cannot follow your claim "stronger procedures and guarantees than what we are getting here". CAs might be useful for a single resource, but we have here a bag of packages and want to distribute the whole repository (with end-to-end signatures). Also, please read the TUF paper and specification which elaborates on the motivation.

And serving sth over http/s and the repository out-of-band opens possible attacks - that's why we decided on a single connection. Git gives us already some linearity/monotonicity conditions.

You should briefly think how opam does updates currently: a repository on GitHub where developers submit their pull requests. This won't change too much.

Guarantees are: if a new package from a new developer is submitted, basically none. The signing of delegation and developer keys (by repository maintainers) enables a web-of-trust style system: once package `foo` has been claimed by the well-known (and signed) developer `alice`, there's no way that `eve` will successfully update `foo` (without getting `alice` key, and also then need to go via GitHub and repository maintainers).