[seL4] Re: General Question On Object Methods

Hello Hugo, The thing is, to fully understand how things work on a low level you can read the seL4 source, it's not that much, it's open and available to everyone. And it's really the best way to find out specific details. So the door is wide open already. People are welcome to ask questions to increase their understanding of how seL4 works, that's how this thread started. Perhaps it's nice to have a medium level description of how seL4 works on a technical level, but it will always describe someone's personal mental model, and will always be a simplification, hence slightly incorrect for some corner cases. However, the seL4 manual is not the place for such info, it's strength is exactly its terseness. Its goal is to give an overview of seL4, if there is too much detail that overview becomes lost and the manual becomes huge and not easily readable any more. The information should be limited to what the user needs to know when using sel4. Giving too much details too early only leads to confusion, people need to build a mental model of how seL4 works first and then they can adjust it when learning more. We can add more information to the website, feel free to open a pull request or open an issue to request specific documentation. I agree that there is so much more to say about seL4, but manpower is limited. Greetings, Indan On 2024-09-11 23:15, Hugo V.C. wrote:

Well, people usually like to understand how things work, moreover on a system like seL4. And, whether you like or not, there will be forks, hacks, modifications... the more info you provide, the more involved the community will be.

Frameworks are a must to speed up real life adoption, but ideally, all the low level info must be clear and the easier the better.

I used to pentest an RTOS derivative of VxWorks on top of some Marvel Armada cpus, at the beginning with public very abstract info, but the fun came when I got (legit) access to confidential low level cpu specs of the different models... then I undestood why some fault injection attacks were being successful.

Developers can do their job with just Mikrokit, but many of them, will have curiosity to understand why they need to do things the way they are forced. By being able to fully understand how things really work at low level, they get more involved, they can also contribute with improvements, and, hopefully, they will be happier than just blindly trust.

It's about letting the door open to developers and engineers to learn at deeper level, as easy as possible.

Maybe a door some people will never open, but for those who dare to open, would be nice to be sure they get engaged.

...

On 12 Sep 2024, at 06:41, Hugo V.C. wrote:

...

"I don’t think tutorials on microkernels and capabilities belong into

...

...

Sure. I have no idea how you guys can deal with this... I'm on the

commercial side, just thinking about how people can "easily" become seL4 developer…

How is this affected by low-level technical details that are hidden behind libraries, especially if you use higher-level frameworks such as

On Wednesday, September 11, 2024, Gernot Heiser via Devel wrote: the seL4 kernel documentation" the Microkit?

...

Gernot