Minutes 29 May 2025

Host: Paul Albertella

Participants: Pete Brink, Gabriele Paoloni, Victor Lu

Agenda

• Discuss some topics from the workshop

Low-level requirements in the kernel

• Attempting to define low-level requirements for a file in the kernel
• See patch
• Document the expectations for the function adjacent to the code, in a way that makes these testable
• This was based on discussion with Tracing subsystem maintainer

Paul: Interesting approach to improving the systematic integrity of the kernel, but completing this is many years of work - what can we do in the shorter term?

Pete: Would prefer to see an iterative approach to this - working down from the system-level objectives to understand what the software is supposed to do, rather than how is it implemented now.

Paul: Interesting aspect of this approach was that it is explicitly thinking about the long-term maintainability of the code in mind. If you describe what each function is intended to do, then it can be re-implemented - for example in Rust!

Discussed the merits of Rust vs C (see slides from workshop), but noted that the language is irrelevant if the intent of the software is not properly understood.

Gab noted that some aspects of the code were difficult to understand without knowledge of the background expectations for the subsystem, and some aspects of the code seemed redundant or related to historical features.

Paul: Might be interesting to document expectations at the subsystem-level rather than at the function level.

Gab: started at the code level because it seemed to be a more immediate way to engage the kernel developer community. Also started with the external interfaces of the subsystem, because this would then make the higher-level expectations clearer. Documentation at the kernel header level is used to build kernel documentation.

Kate is talking to other maintainers to interest them in a similar approach. Interest from Greg K-H.

Pete: If we come up with a set of requirements we have reverse engineered from the code, we should then subject these to safety analysis in order to identify whether there are any gaps - e.g. missing exception-handling.

Using a defined syntax for writing requirements e.g. EARS might have benefits.

Or use something like gherkin to describe tests at a behavioural level.

Next time

Pete: I would like to look at TSF in more detail and identify gaps from a safety perspective