Minutes 07 Mar 2024

Host: Paul Albertella

Participants: Pete Brink, Luigi Pellecchia, Daniel Weingaertner, Florian Wuehr, Alessandro Carminati, Gabriele Paoloni, Igor Stoppa

Discussion:

Continuing discussion from email thread in LFSCS: https://lists.elisa.tech/g/linux-features/topic/restarting_lfscs_operations/104771070

• Igor: Trying to establish approach before we even start trying to argue about a given claim:
  • it is necessary to create a foundation of First Principles
  • it is necessary to understand safety requirements in the light of the first principles
  • it is necessary to define a set of clear problems: why they are relevant, when they are relevant, how they affect safety

Idea is to try to establish these as a basis for cooperation / parallel work in different WGs

Three contributed documents were an attempt to articulate these: https://github.com/elisa-tech/wg-osep/tree/main/Contributions

Igor: Proposed starting point: “Linux is a problem, how do I deal with this?”

• And is this viable, or would it be better to deal with the risk elsewhere?

Pete: What do we mean by first principles?

• Could mean the principles of software engineering
• Igor: I mean something that we can agree is verifiable truth
  • e.g. Given a monolithic OS, anything running in EL1 can interfere with anything else in EL1 and anything else in the process map
  • Statements that are the basis of any set of subsequent claims we make
  • e.g. Any mitigation must explain how these truths are dealt with

Luigi: So we could document these principles?

• Igor: That is what I have done in my document
  • Not exhaustive, but this list of potential interferences must be taken into account
  • Need to show how they are accounted for, or why they are not applicable

Gab: Need to establish a set of safety claims that we are trying to make in order to test these

Paul: This was were we were trying to go with our example:

“I have a bash process (representing a typical process with an assigned safety function) that I would like to protect from interference with its working memory.”

• This can then dictate what our requirements on the kernel actually are.

Gab: How can this help to coordinate work in different working groups, or enable them to collaborate?

• e.g. Alessandro’s proposal for LFSCS - how can Igor’s documents feed into this?

Igor: If you can’t make a FFI claim, then any other claims you make are suspect

• Paul: But we don’t need to have an absolute FFI claim
  • we only need to be able to state for our specific claim, either the identified forms of interference do not apply, or are mitigated
• Igor: And that then becomes a question of how your prove these claims, which is a different problem

Next steps?

• Alessandro: LFSCS should review Igor’s principles / interferences to:
  • confirm that they are accepted,
  • suggest others
  • look for how the interference might be mitigated
• Pete & Luigi: Would prefer to work through the 'bash' use case in OSEP
• Gab: Should we then do some safety analysis in SA on this basis (i.e. the bash use case)?
  • Igor: Want to keep with the bash use case in OSEP
    • Perhaps better to apply the same principles to the Telltale/Watchdog use case in SA?