[seL4] Re: interested in participating in a survey on seL4 website and docsite structure next week?
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 wrote: > > 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. --- ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: interested in participating in a survey on seL4 website and docsite structure next week?
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
[seL4] Re: interested in participating in a survey on seL4 website and docsite structure next week?
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) ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: interested in participating in a survey on seL4 website and docsite structure next week?
> "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 Chubbhttps://trustworthy.systems/ Trustworthy Systems GroupCSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: interested in participating in a survey on seL4 website and docsite structure next week?
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. [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. Bob Trower On Wed, Feb 14, 2024 at 12:15 PM June Andronick (seL4 Foundation) wrote: > 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. --- ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
