From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on ip-172-31-74-118.ec2.internal X-Spam-Level: X-Spam-Status: No, score=-1.9 required=3.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.6 Path: eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail From: Doctor Who Newsgroups: comp.lang.ada Subject: Re: The Ravenscar profile and capabilities paradigm Date: Tue, 12 Oct 2021 17:04:40 +0200 Organization: A noiseless patient Spider Message-ID: References: <07f8mgdot9tmh8mqen2ogd5dds2gojoleh@4ax.com> <5671d9c0-2535-43f2-82e5-258eddb7c879n@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Injection-Info: reader02.eternal-september.org; posting-host="029ba4d39744cc2f920d1f90b5831eec"; logging-data="9097"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19vdJCmwSuwjfeEkki5XOw3" User-Agent: ForteAgent/8.00.32.1272 Cancel-Lock: sha1:Aj4LedcAFcptI8OKzJOpq3TsG+g= Xref: reader02.eternal-september.org comp.lang.ada:62976 List-Id: On Tue, 12 Oct 2021 12:58:48 +0100, "Luke A. Guest" wrote: > >On 12/10/2021 12:51, Richard Iswara wrote: > >>>>> there isn't any existing OS that provides capability-security from the >>>>> ground up, I intend to implement my own. >>>>> >>>> seL4? The whitepaper includes the proofs also. >>> eh yes, I forgot seL4, however it isn't much used I think >> Has Qualcomm and Apple iOS abandoned it when it changed from OKL4 to seL4? >> I thought they use it for isolating their modem firmware from general OS. >> > >The biggest flaw in L4 I found is that sigma0 cannot claim memory back >from processes when it runs out. There was apparently work being done, >but I don't know if they did it. in any case CapROS development is starting again and it promises to be really interesting