interested in participating in a survey on seL4 website and docsite structure next week?
Hi, We are working on improvements to the seL4 website (https://sel4.systems/) and docsite (https://docs.sel4.systems/) Next week, we will conducting a survey (over a week) to gather feedback on the website and docsite structures. If you’re interested in participating, please email me at june@sel4.systems Thanks June
Note that the website is good. It is mercifully free
of distracting elements and vanilla links make it easy to navigate. That's
good. This note is about the inability to just quickly hack on the system
through a quick link and simple procedure.
I would like to be able to go to the main page, click on a download
button, download a pre-built VM, under something dead simple like
VirtualBox, log in and build code.
<freelyignore>
[Note: This sounds a bit ranty. Sorry. I don't mean it to offend. I am just
trying to communicate that assumptions about the environment and
participants are a barrier to entry for people who might otherwise be able
to pitch in.]
It would be nice if a person did not have to spend tons of time getting
into the culture and jumping through endless hoops to simply get into a
sel4 system to see if they can hack on it.
I have worked in dozens of places over the years and everybody thinks that
their (latest) way of doing things is how everybody does things. They are
incorrect.
People like me are doing stuff. We cannot make the time to immerse
ourselves in an elaborate culture with all of its idioms and
particularities.
One of the reasons a horrible language like Python has taken hold is that
like it or not you can pretty easily get to something that works with pip.
Same with the nightmare scene that is JS with npm.
When you are stuck installing multiple entire packages of things in order
to get something to work you more often than not find that something,
somewhere, is broken.
I am working on other things, but my hope was to ultimately target sel4 for
delivery so that it would be somewhat feasible to prove the security of a
custom RISC-V->sel4->app to at least have a plausibly secure device. I
still have that hope, as I see ongoing progress over the years, but it
would be nice to be able to hack on a live system from time to time to
prove out various things.
I went through ridiculous hoops to figure out how to sign a VirtualBox VM.
I did so because I want to be able to release something actually buildable
and usable 'out of the box', so dependencies as tested are all in place.
https://blog.bobtrower.com/2024/01/code-signing-and-virtual-box-vm.html
I like to build dead-vanilla precisely so I don't have to work on shifting
sand. My hope is to release a signed working build environment in an
operating system image suitable for easy delivery and verification.
I appreciate how extraordinarily difficult it can be to work with all these
moving parts and assemble things for delivery. However, I think that
working to have a known image that is known to work and can be checked for
validity with a hash, and a verifiable code signing signature might pay for
itself in terms of lessening the amount of back and forth trying to correct
environmental differences, and in lowering the barrier to entry for
programmers who have skill, but not familiarity with all of the ins and
outs of your particular way of doing things.
Things like "it works on my machine" should not be the response to someone
having a problem with a build.
</freelyignore>
Bob Trower
On Wed, Feb 14, 2024 at 12:15 PM June Andronick (seL4 Foundation)
Hi,
We are working on improvements to the seL4 website (https://sel4.systems/) and docsite (https://docs.sel4.systems/)
Next week, we will conducting a survey (over a week) to gather feedback on the website and docsite structures.
If you’re interested in participating, please email me at june@sel4.systems
Thanks June _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
-- Bob Trower --- From Gmail webmail account. ---
"Bob" == Bob Trower
writes: Bob> I would like to be able to go to the main page, click on a Bob> download button, download a pre-built VM, under something dead Bob> simple like VirtualBox, log in and build code.
It's not _quite_ as simple as that, but did you try the Docker instructions at https://docs.sel4.systems/projects/dockerfiles/ ? The Docker container has all the dependencies for seL4test and most CAmkES projects; and there's a simple workflow described for getting at both the source you want to work on (using whatever tools you want) and a compilation environment. Using the Microkit is a different matter; and one we're still working on. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
On 2/16/24 18:01, Peter Chubb via Devel wrote:
"Bob" == Bob Trower
writes: Bob> I would like to be able to go to the main page, click on a Bob> download button, download a pre-built VM, under something dead Bob> simple like VirtualBox, log in and build code. It's not _quite_ as simple as that, but did you try the Docker instructions at https://docs.sel4.systems/projects/dockerfiles/ ?
The Docker container has all the dependencies for seL4test and most CAmkES projects; and there's a simple workflow described for getting at both the source you want to work on (using whatever tools you want) and a compilation environment.
Using the Microkit is a different matter; and one we're still working on.
Would it be possible to ensure that the container images are signed and that their builds verify either the signatures or hashes of everything they download? -- Sincerely, Demi Marie Obenour (she/her/hers)
On 18 Feb 2024, at 03:49, Demi Marie Obenour
The mannerly answers from everybody are much appreciated.
[Elided rant]
I am heartened by the notion that some thought has already been given to
this with Docker.
If I find the time to install this, I will take a look and see if it can be
packaged under a VM I am able to sign.
Meantime, thanks for being gracious about my interruption. Note that I am
easy to find online and if there is some question you have that you think I
can answer feel free to let me know.
B.
On Sat, Feb 17, 2024 at 8:03 PM Gerwin Klein via Devel
On 18 Feb 2024, at 03:49, Demi Marie Obenour
wrote: On 2/16/24 18:01, Peter Chubb via Devel wrote: It's not _quite_ as simple as that, but did you try the Docker instructions at https://docs.sel4.systems/projects/dockerfiles/ ?
The Docker container has all the dependencies for seL4test and most CAmkES projects; and there's a simple workflow described for getting at both the source you want to work on (using whatever tools you want) and a compilation environment.
Using the Microkit is a different matter; and one we're still working on.
Would it be possible to ensure that the container images are signed and that their builds verify either the signatures or hashes of everything they download?
That might be possible. Almost everything it downloads is via apt-install already.
I've opened an issue for it.
Cheers, Gerwin
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
-- Bob Trower --- From Gmail webmail account. ---
participants (5)
-
Bob Trower
-
Demi Marie Obenour
-
Gerwin Klein
-
June Andronick (seL4 Foundation)
-
Peter Chubb