@ariadne Never head of VxWorks either. What I have heard of though are #Genode & #seL4.

Unlike those two, VxWorks isn't confident-enough to have their code available for inspection, that's not a good sign.

Wonder what it would take to set up a #seL4 dev workstation. Hardware choices would be very restrictive I'm sure. Would it be capable of running many of the programs I need?

So this is a thing that happened: ACM Software Systems award for #seL4
Gerwin, June and Rafal, the 3 founders of Proofcraft, have received, together with their former colleagues at the Trustworthy Systems group, the prestigious ACM Software System Award, for the “development of the first industrial-strength, high-performance operating system to have been the subject of a complete, mechanically-checked proof of full functional correctness”.
https://proofcraft.systems/news-2023/#2023-05-04

Stoked to be part of an awesome team that has won the ACM Software System Award for the creation and real-world deployment of the #seL4 microkernel https://awards.acm.org/software-system

Happy 3rd birthday, #seL4 Foundation!

Next in our #EverythingOpen Speaker Spotlight, we have Ivan Velickovic and Lucy Parker from the #TrustworthySystems group at #UNSW who will present on #sel4 Core Platform:

https://2023.everythingopen.au/schedule/presentation/35/

Excited to join other innovators from the world of high assurance at the seL4 Summit 2023 in Minneapolis, Minnesota this fall! 🎉

Our Embedded Software Engineer, Robbie V., is a part of the program committee for this annual international summit -- the perfect opportunity to learn about the world's most highly assured OS kernel, seL4, and connect with the seL4 community. 💡

From sharing exciting developments to learning about the latest progress in seL4 technology, this is an event you won't want to miss! 💥 🚀

https://sel4.systems/Foundation/Summit/2023/

#sel4 #sel4summit #embeddedsoftware #minneapolis

Do you have a customer who needs specific specs for their embedded core but can't find a market core that meets the requirements?

Previously, the only options were to use a market core that supports virtualization but doesn't meet the customer's spec or to create a custom RISC-V core but lose virtualization support.

Now, you no longer have to choose between meeting your customer's core specs and providing virtualization support.

We have the solution for those looking for high assurance embedded systems with virtualization.

DornerWorks can help you meet both of these requirements with a seL4 microkernel based foundation and RISC-V architecture -- the ideal solution for companies that need virtualization but want to avoid licensing fees and royalties.

Here's how: https://dornerworks.com/blog/sel4-on-risc-v-rocket-chip/?utm_medium=&utm_source=Mastodon&utm_campaign=seL4&utm_term=02072023

#RISCV #seL4 #Embedded #Engineering

Time to take this account a bit more online. By way of #Introduction: Hi, I'm Gerwin. I prove things about software in the Isabelle/HOL theorem prover. Theorem proving is fun and easy.

Many of my proofs these days are about the #seL4 microkernel. I'm a co-founder of Proofcraft where we provide services, consulting and training around formal proofs, and in particular around seL4.

I'm also a Conjoint Professor at UNSW where I teach software verification.

@requiem @cstanhope I was hoping to find some docs on #seL4 but I regret to inform that I did not find a clear guide on writing software on top of seL4 running as a #hypervisor.

Looks like they just have some brief docs on running their tests, and a wishlist item of porting Minix 3 as a guest OS. But maybe you can find something that I couldn't:

https://docs.sel4.systems/GettingStarted

E. de Matsos and M. Ahvenjärvi, "seL4 Microkernel for virtualization use-cases: Potential directions towards a standard VMM"¹

Virtualization plays an essential role in providing security to computational systems by isolating execution environments. Many software solutions, called hypervisors, have been proposed to provide virtualization capabilities. However, only a few were designed for being deployed at the edge of the network, in devices with fewer computation resources when compared with servers in the Cloud. Among the few lightweight software that can play the hypervisor role, seL4 stands out by providing a small Trusted Computing Base and formally verified components, enhancing its security. Despite today being more than a decade with seL4 microkernel technology, its existing userland and tools are still scarce and not very mature. Over the last few years, the main effort has been put into increasing the maturity of the kernel itself and not the tools and applications that can be hosted on top. Therefore, it currently lacks proper support for a full-featured userland Virtual Machine Monitor, and the existing one is quite fragmented. This article discusses the potential directions to a standard VMM by presenting our view of design principles and feature set needed. This article does not intend to define a standard VMM, we intend to instigate this discussion through the seL4 community.

#arXiv #ResearchPapers #seL4 #VMM #Virtualisation #Microkernels
__
¹ https://arxiv.org/abs/2210.04328

Good evening good folx of the :fediverse: It's time for your evening #ConnectionList #Introduction. Please meet:

@ashul is a #WebDev and a #runner, living on #Noongar country in #Perth 🇦🇺 👋

@badri is a #writer and #NonFiction #Editor, on the lookout for pieces of #science, #culture, #history and #philosophy 👋

Dr @annettamallon is an #EndOfLife consultant and #doula, with an interest in #sociology and #SocialResearch. She is a #writer and #mentor on #Lutruwita land #Tasmania 👋

@lathiat is into #linux #ubuntu, #ceph and #OpenStack and maintains Avahi #mDNS. It's always DNS, right?! 👋

@benno You might know him as Jeamland, Benno Has Opinions on #systemd 😆 🇦🇺 Writes about #software, and importantly, the people behind it 👋

@melodytaba is a #PhD candidate #researcher at Sydney Uni, researching #Youth #DigitalHealth #SocialMedia #SciComm 👋

@derek is a #ProductManager who is into #SolarPunk and #sustainability 🇺🇸 👋

@hogesonline is a #computing #teacher, is into #Python 🐍 , is learning #JavaScript and is into #cycling 👋
life goal: ✅ 🤣

Distinguished Professor @gernot heads up the #TrustedSystems #systems group at UNSW and is the the founding Chairman of #seL4 - the world's most assured #linux #kernel. 🇦🇺 👋

@estark works on #security and #PKI for Chrome browser - #HTTPS, #certs, #encryption and the like 👋

That's all for this evening, why not consider building your own #ConnectionList? ❤️

Habit: a new functional programming language
"potential for such languages can be seen in recent verified software development projects, such as the construction of the #seL4 microkernel."
https://www.habit-lang.org/#:~:text=potential%20for%20such%20languages%20can%20be%20seen%20in%20recent%20verified%20software%20development%20projects%2C%20such%20as%20the%20construction%20of%20the%20seL4%20microkernel.

Been here a few days, so I guess it’s time for an #introduction post

I’m Alex, better know as Axman6 pretty much everywhere you can think of - IRC (libra.chat#haskell etc.), 🦤 site, probably LinkedIn and others too.

As far as jobs and hobbies are concerned, I’ve been a professional #Haskell developer for nearly a decade, with various roles in finance and #HFT (despite not really having much of an interest in finance…), in the public sector where I worked on much of the #RenewableEnergy parts of https://nationalmap.gov.au at #NICTA & #CSIRO, writing backend services in Haskell, doing lots of #geospatial data processing, #SQL, #DevOps and much more.

I’m currently writing #Daml, a dialect of Haskell, for a large financial system but also #LookingForWork - if you’re in need of an experienced remote Haskell dev who loves to make things go fast, I’d love to have a chat.

I’m also doing my Masters in #cybersecurity at #UNSW - oh how I wish there was more overlap between the #cyber and #functional programming worlds… does it all end with #seL4? Let me know!

I’ve got a strong interest in #cryptography, #integrity, as well as #hacking things to see how they work, and love a good #CTF.

On the more personal side of things, I’m based in #Canberra, #australia. As you can see from my profile pic, I’m also a volunteer in the State Emergency Service - I guess you could say I like pin coladas, and talking walks in the rain… in a storm… on your roof… with a chainsaw⛈️

Google announces #KataOS: #Rust userland on top of #seL4:
https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html

It seems to be special-purpose, but there’s a technical vision here that makes more sense to me than the “Rust in Linux” meme. “Rust in Linux” is more of a distraction than anything else.

RT from Antmicro (@antmicro)

Partnered with @GoogleAI to help build Sparrow, a secure ML platform on @risc_v, #OpenTitan & the @rustlang #KataOS based on the #seL4 microkernel using our #opensource simulator @renodeio. See how we enabled #Rust apps & #GDB debugging for their system @GoogleOSS @seL4Foundation

https://twitter.com/GoogleOSS/status/1580952385291452416

Original tweet : https://twitter.com/antmicro/status/1582021107934105601

#Google Announces #KataOS As Security-Focused OS, Leveraging @rustlang & #seL4 Microkernel

https://www.phoronix.com/news/Google-KataOS

Original tweet : https://twitter.com/phoronix/status/1581573349146505217

RT from Gernot Heiser (@GernotHeiser)

Nils Wistoff from ⁦@ETH_en⁩ talking about adding hardware support for preventing running channels on ⁦@risc_v⁩ #seL4 #Summit

Original tweet : https://twitter.com/GernotHeiser/status/1579485210235715584

RT from DornerWorks (@DornerWorks)

RISC-V is a viable option for companies that need virtualization but want to avoid licensing fees and royalties. Here's how we can help enhance your custom @risc_v core with virtualization and the security benefits of the #seL4 microkernel: https://buff.ly/3EpCY0s #RISCV

Original tweet : https://twitter.com/DornerWorks/status/1578438511967219713

RT from Antmicro (@antmicro)

Together w/ @GoogleAI we developed a new version of the sel4-sys crate to enable @rustlang applications for the #seL4 microkernel, including improvements in @risc_v support. Read more on our blog:
https://antmicro.com/blog/2022/08/running-rust-programs-in-sel4/ @seL4Foundation

Original tweet : https://twitter.com/antmicro/status/1564616071646167052