Update Contributions/Linux_Memory_Management_Essentials.md

Co-authored-by: Paul Albertella <[email protected]>
Signed-off-by: Igor Stoppa <[email protected]>

Author: igor-stoppa

Contributions/Linux_Memory_Management_Essentials.md

@@ -123,7 +123,12 @@ The following considerations are of a more deductive nature.
 1. Because of the way pages, fractions and multiples of them are allocated, freed, cached, recovered, there is a complex interaction between system components at various layers.
 2. Even using cgroups, it is not possible to eliminate indirect interaction at the low level between components with different levels of safety integrity (e.g. the recirculation of pages related to critical processes in one group might be affected by less critical processes in another group)
 3. Because of the nature of memory management, we cannot rule out the possibility that memory management mechanisms will interfere with safe processes, either due to a bug or due to the interference toward the metadata they rely on. For example, the memory management might hand over to a requesting entity a memory page that is currently already in use either by a device driver or by a userspace process playing a role in a safety use case.
-4. These complex interaction between processes, kernel drivers and other kernel code mean that it is practically impossible to qualify the kernel through positive testing alone.
+4. These complex interaction between processes, kernel drivers and other kernel code mean that it is not feasible to qualify the kernel through positive, requirement-based testing alone. 
+   1. Safety-related claims made for the kernel must be specified and verified with a credible set of tests, which must necessarily include negative tests to demonstrate the effectiveness of any detection, mitigation and exception-handling mechanisms provided in support of these claims. 
+   2. Credible analysis of the kernel could be used to devise a suitable set of tests for this, to verify the kernel's behaviour (and/or mitigations provided by other components of a target system) for a documented set of failure modes.
+   3. Specifying requirements and implementing a credible set of tests to cover all of the kernel's functions for the general case is certainly infeasible (and arguably impossible), because the range of potential applications and integrations for Linux is too broad.
+   4. Demonstrating that claims are supported with a combination of analysis and testing does not allow us to argue that the kernel is devoid of a certain class of bug, only that our verification mechanisms are sufficient to detect bugs affecting the specified claims, and for the identified failure modes.
+   5.. Claims must therefore be verified for each iteration of the kernel intended for use in a safety-related context, and for the specific configuration and system integration of a target context; the sufficiency of the set of failure modes considered, and of the analysis informing these, must be also confirmed for the target context.
    1. Specifying requirements and implementing a credible set of tests to cover all of the kernel's functions for the general case is certainly infeasible (and arguably impossible), because the range of potential applications and integrations for Linux is too broad.     
    2. We can constrain this scope by specifying a kernel version and configuration, for a given set of target systems and software integrations, and specifying the set of functions it is intended to provide. However, this would still not be sufficient to assert that the kernel is devoid of certain classes of bug (e.g. for bugs caused by interference).     
    3. Negative tests derived from credible analysis of the kernel could be used to address this, by verifying its behaviour (and/or mitigations provided by other components of a target system) for a documented set of failure modes.