Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Sel4: We’re going open source

sel4.systems

Post reply on HN
Print view View original

21–30 of 65 posts

Re: Sel4: We’re going open source

#21

Post by blahbl4hblahtoo »

luckydude wrote: post #2

"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?

From the paper "Comprehensive formal verification of an OS microkernel":

"We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"

http://www.nicta.com.au/pub?doc=7371

There's a lot of assuming going on...I'm not saying that what they've done isn't interesting, but as always don't let yourself get carried away.

Re: Sel4: We’re going open source

#22

Post by moblahbl4hblah »

luckydude wrote: post #2

"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?

From the paper "Comprehensive formal verification of an OS microkernel": "We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"

http://www.nicta.com.au/pub?doc=7371

There's a lot of assuming going on...I'm not saying that what they've done isn't interesting, but as always don't let yourself get carried away.

Re: Sel4: We’re going open source

#23

Post by wmf »

Avshalom wrote: post #19
TacticalCoder wrote: post #17

Earlier quoted context omitted.

Concerning the compiler, in the link it is written: "There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary." (I wonder how that works but it is related to your compiler concern) Now even though the issue of hardware (say rogue hardware wi…

On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.

What if the code doesn't rely on undefined behavior?

Re: Sel4: We’re going open source

#24

Post by StefanKarpinski »

This is an awful lot of fanfare for the open sourcing of something that was funded with public money by the government of Australia, using open source tools and technologies. Why isn't it already open source?

In general, I would like to see more software developed with public research funding required to be open source as part of the grant stipulation, ideally from early on. Too often tax-payer money is used to develop software which then ends up being closed source and providing profit to some commercial entity, instead of benefiting, you know, the people who payed for it – the public.

Re: Sel4: We’re going open source

#25

Post by regehr »

wmf wrote: post #23
Avshalom wrote: post #19

Earlier quoted context omitted.

On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.

What if the code doesn't rely on undefined behavior?

Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.

Re: Sel4: We’re going open source

#26

Post by hackuser »

Could someone with expertise in this area share what is really meant by "end-to-end proof of implementation correctness and security enforcement", and the practical implications of it? The words suggest that the kernel is 'proven' to be absolutely secure, which obviously is false (and I don't think the authors are trying to make that claim). So what are the precise implications for confidentiality, availability, and integrity?

Re: Sel4: We’re going open source

#27

Post by pron »

hackuser wrote: post #26

Could someone with expertise in this area share what is really meant by "end-to-end proof of implementation correctness and security enforcement", and the practical implications of it? The words suggest that the kernel is 'proven' to be absolutely secure, which obviously is false (and I don't think the authors are trying to make that claim). So what are the precise implications for confidentiality, availability, and…

Perhaps they've proven that privilege escalation is impossible.

Re: Sel4: We’re going open source

#28

Post by hershel »

hackuser wrote: post #26

Could someone with expertise in this area share what is really meant by "end-to-end proof of implementation correctness and security enforcement", and the practical implications of it? The words suggest that the kernel is 'proven' to be absolutely secure, which obviously is false (and I don't think the authors are trying to make that claim). So what are the precise implications for confidentiality, availability, and…

Here they describe it in detail:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Basically they plugged a lot of the possible holes, but it's not done yet.

Re: Sel4: We’re going open source

#30

Post by nl »

StefanKarpinski wrote: post #24

This is an awful lot of fanfare for the open sourcing of something that was funded with public money by the government of Australia, using open source tools and technologies. Why isn't it already open source? In general, I would like to see more software developed with public research funding required to be open source as part of the grant stipulation, ideally from early on. Too often tax-payer money is used to devel…

Why isn't it already open source?

Not sure if you are Australian or not, but - unlike the in the US - in Australia there is no assumption that publicly funded work will be in the public domain.

Generally the way it works here is that bodies like Nicta (and CSIRO) are expected to make a return on the investments that are made in them - ie, they are expected to make money somehow. The default way they do that is generally IP licensing.

Personally I think this is very short sighted, but it shouldn't surprise anyone.

Post reply on HN