Hi Isaac
> "Isaac" == Isaac Beckett writes:
Isaac> Hello! Looking at the LionsOS website and documentation you
Isaac> posted, it seems like Lions is an operating system built using
Isaac> Microkit out of components/drivers that use the sDDF? Do I have
Isaac> the right shape of things in my h
Sorry, I should clarify. I meant making a dynamic OS that uses the sDDF. Not on
Microkit, since it’s not meant for that. But something that is more flexible at
runtime, designed for general purpose use so that it can load components when
they’re needed instead of having a fixed set of components
On 4/17/24 18:02, Isaac Beckett wrote:
> Sorry, I should clarify. I meant making a dynamic OS that uses the sDDF. Not
> on Microkit, since it’s not meant for that. But something that is more
> flexible at runtime, designed for general purpose use so that it can load
> components when they’re nee
On 18 Apr 2024, at 13:13, Demi Marie Obenour wrote:
properly implements mitigations. Time protection is a principled solution
to side-channel attacks, but it requires that the time consumed by operations
on sensitive data is not observable.
This is actually not a correct summary of time protect
On 18 Apr 2024, at 08:02, Isaac Beckett wrote:
Sorry, I should clarify. I meant making a dynamic OS that uses the sDDF. Not on
Microkit, since it’s not meant for that. But something that is more flexible at
runtime, designed for general purpose use so that it can load components when
they’re n
On 4/17/24 23:20, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 13:13, Demi Marie Obenour wrote:
>
> properly implements mitigations. Time protection is a principled solution
> to side-channel attacks, but it requires that the time consumed by operations
> on sensitive data is not observab
On 18 Apr 2024, at 13:40, Demi Marie Obenour wrote:
>
>
> How does time protection handle these two cases?
>
> 1. Untrusted code can request a service from trusted code that involves
> processing sensitive data, and this request may take an unbounded
> amount of time. In this case, it is n
"A web browser is a good example of this. The number of security
domains is at least the number of origins in use, which can be
extremely large. Furthermore, some origins might be CPU-intensive."
Yes. That's the challenge when you try to use a solution aimed to static
systems for dynami
On 18 Apr 2024, at 19:18, Hugo V.C. wrote:
>
> "A web browser is a good example of this. The number of security
> domains is at least the number of origins in use, which can be
> extremely large. Furthermore, some origins might be CPU-intensive."
>
> Yes. That's the challenge when you tr
"All this is a matter for user mode. "
Well... in seL4. In standard OSs (Windows, Linux...) this is a matter of
kernel mode. And here is the party. Of course if you use seL4 as TCB then
you can partition whatever you want on top.
The challenge that I probably didn't expressed correctly, is to in
On 18 Apr 2024, at 20:38, Hugo V.C. wrote:
The challenge that I probably didn't expressed correctly, is to integrate seL4
on top of other dynamic systems (in example to virtualize a browser), as seL4
needs to know in advance how much memory will have available... Running seL4 on
bare metal is
On 18/04/24 12:12, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 20:38, Hugo V.C. wrote:
>
> The challenge that I probably didn't expressed correctly, is to integrate
> seL4 on top of other dynamic systems (in example to virtualize a browser), as
> seL4 needs to know in advance how much m
"Running seL4 in any way other than on bare metal makes no sense
whatsoever."
There are scenarios where it makes sense. The power of seL4 is isolation
guarantee. That is, software running virtualized on top of seL4 can't
escape from seL4. This means it can be used to safely run a web browser
(virt
On 4/18/24 05:34, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 19:18, Hugo V.C. wrote:
>>
>> "A web browser is a good example of this. The number of security
>> domains is at least the number of origins in use, which can be
>> extremely large. Furthermore, some origins might be CPU-
On 4/18/24 07:12, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 20:38, Hugo V.C. wrote:
>
> The challenge that I probably didn't expressed correctly, is to integrate
> seL4 on top of other dynamic systems (in example to virtualize a browser), as
> seL4 needs to know in advance how much me
"running seL4 in a virtualized environment makes a huge amount
of sense for testing and debugging, or if one is shipping a virtual
appliance."
or running on top of any other standard OS... Those are latest news (April
17th):
"*Google and Mozilla on Tuesday announced security updates that address
Hello Hugo,
On 2024-04-19 10:06, Hugo V.C. wrote:
1) Let's forget the naive idea of users changing behavior or vendors
making
secure software. Users are "ignorant" and vendors are unethical. That's
raw
reality.
Both Chromium and Firefox are open-source. Calling Mozilla and all the
volunteers
Hi Indan.
"Both Chromium and Firefox are open-source. Calling Mozilla and all the
volunteers unethical is unkind. Nothing is stopping you and like minded
people from forking and creating a version which is more secure."
I talked about "vendors" in general. Never specified about any particular
ven
Re: "Yes, it is a waste of resources. But it is secure. "
I agree.
I have been thinking of this tradeoff for another security scenario and my
current thinking is:
- It's just necessary
- It's not really a waste. It is a price paid for security and the
security is worth the price.
- What a call
I agree with Gernot.
Ultimately, in deployment as a secure system, isn't the whole point of this
to have confidence that it is in fact secure?
As a practical matter of convenience for development, I would find it much
easier to work with Sel4 in a virtualized environment. However, I would not
hav
I totally agree with the notion that we want to be able to run sel4 in a
virtualized environment for development, debug, testing, and perhaps even
production scenarios where that makes the most sense. However, as Gernot
seems to be stressing, sel4 is supposed to be *secure* and that means the
most
Hello.
There have been many interesting points, but it was a strawman fallacy to
suggest Hugo accused "all the volunteers" of being unethical.
I think Hugo has a salient point when he says a world of bespoke seL4
images for every application is a distant one. I share the feeling that a
hybrid, in
On Fri, Apr 19, 2024 at 3:07 PM Michael Neises wrote:
>
> I think Hugo has a salient point when he says a world of bespoke seL4
> images for every application is a distant one. I share the feeling that a
> hybrid, intermediate step is meaningful. I also echo the idea that
> exploitation at scale i
On Sat, 20 Apr 2024 at 09:33, Andrew Warkentin wrote:
>
> I don't really think the static Microkit/CAmkES type of architecture
> will ever be viable for desktops or self-hosting. Basically nobody's
> going to put up with rebooting into a different image for each
> application like an 80s-era home
24 matches
Mail list logo
