jesse_m
Joined 12 years ago
Karma
55
Submissions
50
Member since
May 19
Recent submissions
Comment · 5 years ago
I love this app. I really like how it shows you tracking images and stuff in the emails.
Comment · 6 years ago
Radicalized is in paperback on Amazon: https://www.amazon.com/Radicalized-Cory-Doctorow/dp/12502292...
It has unauthorized bread in it.
Comment · 6 years ago
Also, he gets more of a cut if you buy from him and no DRM! win-win
Comment · 6 years ago
One thing that seL4 requires is an mmu in order to support the isolation claims. The intel me type cpu would need to have some of these features that micorcontrollers don't usually have.
Comment · 6 years ago
That's not necessarily true. There are VMM or hypervisor projects that utilize seL4 for x86 and ARM [1][2][3]. In this situation there isn't really one that is in "control". You could also have other threads or components that have higher privileges that can maybe do other monitoring or control activities.
1: https://github.com/seL4/camkes-vm 2: https://github.com/seL4/camkes-vm-examples 3: https://github.com/SEL4PROJ/camkes-arm-vm-manifest
Comment · 6 years ago
For what it's worth, the current draft of the hypervisor extensions is available here: https://github.com/riscv/riscv-isa-manual/releases/download/... and is Chapter 5
It does say this: The hypervisor extension has been designed to be efficiently emulable on platforms that donot implement the extension, by running the hypervisor in S-mode and trapping into M-modefor hypervisor CSR accesses and to maintain shadow page tables. The majority of CSR accessesfor type-2 hypervisors are valid S-mode accesses so need not be trapped. Hypervisors can supportnested virtualization analogously.
Comment · 6 years ago
Is the ports system similar to Gentoo's portage/ebuild system? I can get sources, configure the build, or get binaries (for some things) pretty easy through it.
The QA with the build farm would be nice though.
Comment · 6 years ago
I can't stand the invisible syntax like double trailing space.
Comment · 6 years ago
I can't stand the invisible syntax like a double trailing space is some valid syntax.
Comment · 6 years ago
I think one of the big things here is that the refinement proofs from the models for isolation, IPC fast path, capability access control, and scheduling to C source to binary are strongest when the kernel is built with a particular configuration on particular hardware. When all of these are satisfied and you are on a trusted platform, you have very very strong guarantees that what is modeled is what you get. But it's not like this is hidden. They have make it pretty clear what the verified platforms and configurations are[1].
You should take a look at the verification chain though[1]. It is fairly extensive. It's not like they proved just a small part of a system in a general way.
Comment · 6 years ago
The RISC-V proof is very close to being completed too. Gernot talked at the RISC-V Summit 2019: https://www.youtube.com/watch?v=2IXBoVIUuVI
Comment · 6 years ago
I believe this was the HACMS program. Data61 has some more information: https://ts.data61.csiro.au/projects/TS/SMACCM/
It may be worth mentioning that it isn't the kernel that rebooted the system but some monitoring thread.
Comment · 6 years ago
I think he's talking to the serval mesh guy
Comment · 6 years ago
I haven't heard of the leo editor. I have used org mode in Emacs for little things. I also came across a reimplmentation of the tangling functionality: https://github.com/thblt/org-babel-tangle.py
Comment · 6 years ago
The Embedded Muse
http://www.ganssle.com/tem-subunsub.html
Jack Ganssle has some really good content he's written for other publications as well.