mastouille.fr est l'un des nombreux serveurs Mastodon indépendants que vous pouvez utiliser pour participer au fédiverse.
Mastouille est une instance Mastodon durable, ouverte, et hébergée en France.

Administré par :

Statistiques du serveur :

597
comptes actifs

#sel4

0 message0 participant0 message aujourd’hui
Cyberagentur<p>Ein Meilenstein für IT-Sicherheit: Die <span class="h-card" translate="no"><a href="https://social.bund.de/@Cyberagentur" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>Cyberagentur</span></a></span> hat am 20.01.2025 fünf Verträge für das Forschungsprogramm „Ökosystem vertrauenswürdige IT“ (ÖvIT) unterzeichnet. Ziele: Beweisbare IT-Sicherheit und ein internationales Netzwerk von Experten.<br>Mehr Informationen: <a href="https://t1p.de/8mb4c" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">t1p.de/8mb4c</span><span class="invisible"></span></a> <br><a href="https://social.bund.de/tags/%C3%96vIT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ÖvIT</span></a> <a href="https://social.bund.de/tags/Cybersicherheit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Cybersicherheit</span></a> <a href="https://social.bund.de/tags/FormaleVerifikation" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormaleVerifikation</span></a> <a href="https://social.bund.de/tags/Forschung" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Forschung</span></a> <a href="https://social.bund.de/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a></p>
HoldMyType<p>Running the manual: an approach to high-assurance microkernel development<br>&gt; the kernel is obviously a state<br>transformer, and hence, conveniently represented as a monad. This<br>choice is reaffirmed by the need for recoverable exceptions, which<br>are detailed in the next subsection. In fact, we will see that we want<br>to distinguish between code that may raise recoverable exceptions<br>and code that does not have that liberty. Hence, it is worthwhile<br>to use monad transformers as provided by the MTL in the Haskell<br>Hierarchical Libraries <br>&gt; seL4 API includes several system calls that<br>attempt to manipulate a capability address space, which is a data<br>structure containing a sparse mapping from addresses to capabili-<br>ties. If one of these system calls fails to locate a specified capability,<br>it will generate a system call error that is returned to the caller. On<br>the other hand, a similar failure while searching for a capability that<br>is being directly invoked will generate a fault message that is sent<br>to the current thread’s fault handler; a failure while trying to trans-<br>mit a capability through a one-way communication channel will be<br>silently ignored when the receiver is unable or unwilling to receive<br>the capability.<br>&gt; HOL is a logic of total functions and is as such not suitable to ex-<br>press the semantics of Haskell directly. It is however suitable to<br>describe the semantics of Haskell functions that always terminate<br>and that do not make essential use of laziness. The seL4 implemen-<br>tation consists of such functions.</p><p><a href="https://mathstodon.xyz/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>haskell</span></a> <a href="https://mathstodon.xyz/tags/isabelle" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>isabelle</span></a> <a href="https://mathstodon.xyz/tags/sel4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4</span></a><br><a href="http://portal.acm.org/citation.cfm?id=1159842.1159850&amp;coll=portal&amp;dl=ACM&amp;type=series&amp;idx=1159842&amp;part=Proceedings&amp;WantType=Proceedings&amp;title=Haskell&amp;CFID=18785943&amp;CFTOKEN=93152956" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">http://</span><span class="ellipsis">portal.acm.org/citation.cfm?id</span><span class="invisible">=1159842.1159850&amp;coll=portal&amp;dl=ACM&amp;type=series&amp;idx=1159842&amp;part=Proceedings&amp;WantType=Proceedings&amp;title=Haskell&amp;CFID=18785943&amp;CFTOKEN=93152956</span></a></p>
Rob Sison<p>There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_verification</span></a></p>
blake shaw 🇵🇸<p>Oh wow, I wasn't aware that <a href="https://autonomous.zone/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> Foundation has uploaded the lectures of <a href="https://autonomous.zone/tags/UNSW" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>UNSW</span></a>'s famous Advanced Operating Systems course to youtube.</p><p><a href="https://www.youtube.com/watch?v=IvqM2pmApSY&amp;list=PLtoQeavghzr3nlXyJEXaTLU9Ca0DXWMnt" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=IvqM2pmApS</span><span class="invisible">Y&amp;list=PLtoQeavghzr3nlXyJEXaTLU9Ca0DXWMnt</span></a><br><a href="https://autonomous.zone/tags/os" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>os</span></a> <a href="https://autonomous.zone/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://autonomous.zone/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>operatingsystems</span></a></p>
Axman6 | 🇦🇺<p><span class="h-card" translate="no"><a href="https://infosec.exchange/@riskybusiness" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>riskybusiness</span></a></span> RE your discussion about viewing iPhone on macOS - I’m 99% sure this is a direct device to device connection, iCloud isn’t involved other than the devices being on the same account and having shared secrets/keys. </p><p>It’s not that different from the current implementation that lets you use an iPad as a second screen over wifi - it’s designed for the “my phone is in my pocket/over there charging and I don’t want to get it” use case, not the “my phone is at home and I want to stream its screen over the internet” case - unless I’ve missed something? I’d be shocked if it weren’t encrypted using keys in each device’s Secure Enclave. </p><p>Somewhat unrelated, but this also reminds me of some tech DST Group showed me years ago when we were teaching them. It allowed a user to use an untrusted web browser/computer to connect to a Remote Desktop-esque page, but the image was encrypted They had a device which sat between the computer and monitor which decrypted the image signal, and encrypted keyboard/mouse data back to the page. (All built on <a href="https://infosec.exchange/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> of course).</p>
Gernot Heiser<p>Last year when the <a href="https://discuss.systems/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> Team won the ACM Software System Award, most of the awardees agreed to pool the price money for a PhD scholarship. This is now open for applications: <a href="https://trustworthy.systems/students/schol-swsa" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">trustworthy.systems/students/s</span><span class="invisible">chol-swsa</span></a></p>
Gernot Heiser<p><span class="h-card" translate="no"><a href="https://infosec.exchange/@Axman6" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>Axman6</span></a></span> <span class="h-card" translate="no"><a href="https://mastodon.social/@bagder" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>bagder</span></a></span> Well, to be fair, <a href="https://discuss.systems/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> isn't an *Operating System*, it's an OS microkernel with BYO device drivers.<br>However, the Lions OS built on top of it should exit the vapourware phase by the end of the year 😉<br><a href="https://trustworthy.systems/projects/LionsOS/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">trustworthy.systems/projects/L</span><span class="invisible">ionsOS/</span></a></p>
blake shaw 🇵🇸<p>systems beyond <a href="https://functional.cafe/tags/posix" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>posix</span></a>: <a href="https://functional.cafe/tags/sel4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4</span></a></p><p><a href="https://www.youtube.com/watch?v=ekV7wWQf7_g" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=ekV7wWQf7_</span><span class="invisible">g</span></a><br><a href="https://functional.cafe/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://functional.cafe/tags/os" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>os</span></a></p>
blake shaw 🇵🇸<p><a href="https://functional.cafe/tags/Pancake" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Pancake</span></a>: a new, verified Pascal-like <a href="https://functional.cafe/tags/pl" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>pl</span></a> emphasizing formal verification over type safety for low-level systems programming, device drivers in particular.</p><p>"Pancake eschews complex type systems to make the language attractive to systems programmers, while at the same time aiming to ease the formal verification of code. We describe the design of the language and its verified compiler, and examine its usability, performance and current limitations through case studies of device drivers and related systems components for an <a href="https://functional.cafe/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a>-based <a href="https://functional.cafe/tags/os" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>os</span></a>." </p><p><a href="https://trustworthy.systems/publications/papers/Pohjola_STWSNUMSMNH_23.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">trustworthy.systems/publicatio</span><span class="invisible">ns/papers/Pohjola_STWSNUMSMNH_23.pdf</span></a><br><a href="https://functional.cafe/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://functional.cafe/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a></p>
blake shaw 🇵🇸<p>Explaining the <a href="https://functional.cafe/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> integrity theorems</p><p><a href="https://www.youtube.com/watch?v=fyF9w_CsCEU" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=fyF9w_CsCE</span><span class="invisible">U</span></a><br><a href="https://functional.cafe/tags/hol" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>hol</span></a> <a href="https://functional.cafe/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://functional.cafe/tags/os" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>os</span></a> <a href="https://functional.cafe/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://functional.cafe/tags/isabelle" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>isabelle</span></a></p>
blake shaw 🇵🇸<p>The formalization of <a href="https://functional.cafe/tags/sel4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4</span></a> in <a href="https://functional.cafe/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> on <a href="https://functional.cafe/tags/TypeTheoryForall" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheoryForall</span></a> podcast<br><a href="https://www.typetheoryforall.com/2023/02/04/27-Gerwin-Klein.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">typetheoryforall.com/2023/02/0</span><span class="invisible">4/27-Gerwin-Klein.html</span></a></p>

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? ❤️

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 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⛈️

nationalmap.gov.auTerria MapA web map built on Terria Map

Google announces #KataOS: #Rust userland on top of #seL4:
opensource.googleblog.com/2022

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.

Google Open Source BlogAnnouncing KataOS and SparrowWe've open sourced several components for our secure operating system, called KataOS, on GitHub, as well as partnered with Antmicro