<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div><br>
</div>
<div>Paul Sherwood wrote:</div>
<div><br>
</div>
<div>“<i>I understand the argument, but this last sentence is flawed.</i></div>
<i><br>
The fact that some statements are not covered by tests does not necessarily<br>
mean that they have never been tested. For example the Linux community<br>
benefits from the fact that their software is tested on billions of<br>
</i>
<div><i>devices every day.</i>”</div>
<div><br>
</div>
<div>Sorry, I’m not buying that argument. Counter-example? Heartbleed. It was reported to have been introduced into OpenSSL's TLS in 2012 and apparently not discovered by “the good guys” until 2014. That no “normal” code triggered the buffer overrun certainly
did not at all mean that the buffer overrun defect wasn’t there. Who knows how many times that defect was maliciously exploited before it was finally discovered by "the good guys” and eliminated?</div>
<div><br>
</div>
<div>And Heartbleed was in software that WAS supposedly tested—the issue being that the testing that was done was obviously inadequate to reveal that defect.</div>
<div><br>
</div>
<div>Given the rank amateur-ish manner in which the vast majority of software is produced these days—particularly in the open source community—there can be no substitute for
<b><i><u>truly comprehensive</u></i></b> testing to have any trust at all in that code.</div>
<div><br>
</div>
<div><br>
</div>
<div>— steve</div>
<div><br>
</div>
<div><br>
</div>
<br id="lineBreakAtBeginningOfMessage">
<div><br>
<div>On Aug 6, 2024, at 10:35 AM, Paul Sherwood <paul.sherwood@codethink.co.uk> wrote:</div>
<br class="Apple-interchange-newline">
<div>
<div>Hi Dewi<br>
<br>
Please see my comments inline...<br>
<br>
On 2024-08-06 14:27, Dewi Daniels wrote:<br>
<blockquote type="cite">
<blockquote type="cite">What do you mean by Linux, here? If you are meaning "the people who<br>
develop Linux", then I think the reason is that they have been able<br>
to<br>
achieve their goals for the software without compliance. In almost<br>
all<br>
cases the developers will not have needed to consider those specific<br>
standards at any point during their careers.<br>
</blockquote>
So, the problem is not that Linux cannot meet the relevant standards,<br>
but that there is no motivation for the Linux developers to comply<br>
with the standards?<br>
</blockquote>
<br>
In general that is correct, yes. And actually this concern will be<br>
compounded (or perhaps even detonated) by the European Cyber Resilience<br>
Act [1].<br>
<br>
<blockquote type="cite">Surely, if Linux is to be used for safety<br>
applications, there needs to be a 'Safe Linux' branch that complies<br>
with the relevant standards.<br>
</blockquote>
<br>
I believe that some organisations are still attempting that, but doubt<br>
that they will succeed.<br>
<br>
<snip><br>
<blockquote type="cite">I accept that before I started writing safety-critical software, I<br>
didn't necessarily test every single line of code. Dave Thomas, who I<br>
used to work for, says in his presentation Agile is Dead • Pragmatic<br>
Dave Thomas • GOTO 2015 (youtube.com) [1] at 18:00 that he doesn't<br>
test everything. However, there is a big difference between safety<br>
applications and other kinds of applications. Even IEC 61508 SIL 1 or<br>
DO-178C Level D is a very strong claim. Since I started writing<br>
safety-critical software, I have tended to test everything just<br>
because it isn't that hard and doesn't take that much time.<br>
</blockquote>
<br>
I agree that everything should be tested.<br>
<br>
<blockquote type="cite">DO-178C doesn't require you to achieve 100% structural coverage<br>
through unit tests. It requires that your requirements-based tests<br>
(which can be hardware/software integration tests, software<br>
integration tests or low-level tests) cover all the software<br>
requirements and exercise all the code. If your tests haven't covered<br>
all the requirements, there's functionality you haven't tested. If<br>
your tests haven't achieved statement coverage, then there's code that<br>
you've never executed, not even once, during your testing.<br>
</blockquote>
<br>
I understand the argument, but this last sentence is flawed.<br>
<br>
The fact that some statements are not covered by tests does not necessarily<br>
mean that they have never been tested. For example the Linux community<br>
benefits from the fact that their software is tested on billions of<br>
devices every day.<br>
<br>
Moreover, even in the dwindling population of systems where folks are<br>
still aiming for 100% coverage, there will still be bugs and issues.<br>
Coverage does not guarantee anything.<br>
<br>
<snip><br>
<blockquote type="cite">
<blockquote type="cite">Irrespective of personal preference, I would expect that if Red Hat<br>
chooses to increase test coverage on any project, they are entirely<br>
capable of doing so.<br>
</blockquote>
You claim they are capable of doing so, but they choose not to. It<br>
comes back to the point above that they don't see a commercial<br>
incentive to create a DO-178C or IEC 61508 variant of Red Hat Linux.<br>
</blockquote>
<br>
I can't comment further - I have no affiliation with Red Hat.<br>
<br>
<snip><br>
<blockquote type="cite">There are open-source repositories that are suitable for use in<br>
critical systems. One example is AdaCore's GNAT Ada compiler. Most<br>
open-source projects (and I suspect most proprietary software<br>
projects), even those sponsored by large companies, do surprisingly<br>
little testing. For example, I reviewed part of the ARM Trusted<br>
Computing Platform on behalf of the CHERI Standards Compliance (STONE)<br>
project CHERI+STONE+-+Final+Report+-+for+publication+v1.0.pdf<br>
(squarespace.com) [2]. The System Control Processor (SCP) firmware<br>
consisted of 381,512 SLOC, but there were only 5,291 SLOC of tests.<br>
There are very few open-source projects that do enough testing to<br>
achieve even DO-178C Level D or IEC 61508 SIL 1.<br>
</blockquote>
<br>
I believe you.<br>
<br>
<snip><br>
<blockquote type="cite">
<blockquote type="cite">As stated, previous initiatives have failed to achieve<br>
certification,<br>
but this does not mean that Linux has not been deployed in critical<br>
systems.<br>
</blockquote>
How was it deployed in critical systems if it was not certified?<br>
</blockquote>
<br>
Again, not my stories to tell. But please accept that I haven't come<br>
here to make false statements.<br>
<br>
<blockquote type="cite">
<blockquote type="cite">
<blockquote type="cite">Route 2s: proven in use. This is not considered practicable for<br>
complex software such as operating systems. This was recognised by<br>
SIL2Linux.<br>
</blockquote>
At the risk of seeming 'insulting' again, it seems to me that the<br>
proven<br>
in use path is practically impossible for anything involving modern<br>
electronics, even before we get to the software.<br>
</blockquote>
Agreed<br>
</blockquote>
<br>
Excellent :-)<br>
<br>
<blockquote type="cite">
<blockquote type="cite">
<blockquote type="cite">Route 3s assessment of non-compliant development. This is a very<br>
sensible way of allowing the use of an open-source operating<br>
</blockquote>
system<br>
<blockquote type="cite">such as Linux (more so than the COTS guidance in DO-278A). Route<br>
</blockquote>
3s<br>
<blockquote type="cite">can be summarised as a. what do we know about the software? b.<br>
</blockquote>
what<br>
<blockquote type="cite">evidence do we have that it works? and c. what happens if it goes<br>
wrong? This was the approach adopted by SIL2Linux. Yet they<br>
</blockquote>
failed.<br>
<blockquote type="cite">I'd like to understand why.<br>
</blockquote>
I have some understanding of why, but it is not my story to tell.<br>
</blockquote>
I would love to know more, since IEC 61508-3 Route 3s seemed a<br>
sensible route for SIL2Linux to take.<br>
</blockquote>
<br>
I agree.<br>
<br>
<snip><br>
<blockquote type="cite">I'm glad that you did not aim to insult. There is a big gap between<br>
safety-critical software that complies with the standards and other<br>
software that does not. That's always been the case. Most software<br>
developers care about features, cost and time-to-market.<br>
Safety-critical software developers have to show that the system can<br>
be shown to be acceptably safe before it enters service. I don't agree<br>
with your use of the term 'modern'. The Airbus Flight Control System<br>
(FCS) and the Linux kernel are both modern software-intensive systems.<br>
They've been developed to meet very different goals and have therefore<br>
been engineered differently.<br>
</blockquote>
<br>
I agree with everything you've said here.<br>
<br>
Nonetheless, I believe that some open source software including the Linux<br>
kernel can be shown to be suitable for use in safety-critical systems,<br>
notwitstanding the authors' chosen processes and testing strategies.<br>
<br>
<blockquote type="cite">
<blockquote type="cite">When reasoning about software for a modern multi-core processor,<br>
with<br>
perhaps a million lines of (uncertified) code hidden as firmware,<br>
the<br>
behaviour is not deterministic, so test coverage will not get there.<br>
</blockquote>
Accepted, but that's why a million lines of uncertified code running<br>
on a multi-core processor, whose behaviour is not deterministic, is<br>
not suitable to be used in a safety application.<br>
</blockquote>
<br>
And yet, folks are doing that, and adding AI. What can possibly go wrong?<br>
<br>
<snip><br>
<blockquote type="cite">
<blockquote type="cite">I did not mean to suggest any lack of verification; there is a huge<br>
amount of work done to verify every Linux release. They just don't<br>
set<br>
much store in measuring code coverage via unit tests.<br>
</blockquote>
This is the aspect I have difficulties with. I accept that the Linux<br>
developers don't set much store in measuring code coverage. DO-178C<br>
doesn't require that you achieve structural coverage through unit<br>
tests, by the way. But if they do as much testing as you claim to<br>
verify every Linux release, it should be straightforward for a 'Safe<br>
Linux' team to fill the gaps to achieve compliance with the relevant<br>
standards.<br>
</blockquote>
<br>
Time passes, but this has not been achieved.<br>
<br>
<blockquote type="cite">If the compliance gaps are large and the Linux developers<br>
rely instead on the extremely large user base reporting any defects<br>
quickly so they can be fixed in the next release, then that isn't good<br>
enough for safety applications.<br>
</blockquote>
<br>
Can we maybe get back to the original point, with this? What is "good enough"?<br>
<br>
- Software in practice on multicore processors exhibits stochastic behaviours<br>
(given your experience, I would be surprised if you actually challenge this?)<br>
<br>
- So we have to measure variances, and then the question is what tolerances<br>
should we be aiming for?<br>
<br>
<blockquote type="cite">You talk a lot about "state of the art".<br>
</blockquote>
<br>
That's because I am attempting to clarify what it is, in preparation for<br>
safety assessments.<br>
<br>
<blockquote type="cite">Linux is a widely-respected,<br>
mature operating system, but it is not "state of the art".<br>
</blockquote>
<br>
Hmmm.<br>
<br>
<blockquote type="cite">I consider<br>
formal methods to be "state of the art".<br>
</blockquote>
<br>
I consider formal methods rather impractical, and still very much<br>
a minority sport, more than 40 years after I was originally exposed<br>
to them.<br>
<br>
But yes, state of the art, of a kind.<br>
<br>
<blockquote type="cite">Microsoft, Amazon Web<br>
Services and Intel all have large formal methods teams. See, for<br>
example, the excellent presentation by Rod Chapman, my former<br>
colleague from Praxis: Automated Reasoning in and… | High Integrity<br>
Software Conference 2024 (his-conference.co.uk) [3]. There is even an<br>
open-source operating system microkernel that has been verified using<br>
formal methods - Home | seL4 [4]<br>
</blockquote>
<br>
sel4 is great, but as far as I know the verification doesn't extend to<br>
drivers, and the behaviour may still be compromised by unexpected<br>
chip/firmware (at least, I remember reading a contrite blog post by the<br>
sel4 team when they were caught out by speculative execution along with<br>
everyone one else). I may be wrong of course.<br>
<br>
<blockquote type="cite">Prof. Peter Ladkin is one of the World's leading experts on practical<br>
statistical evaluation of critical software. Peter has pointed out<br>
that using statistical techniques to measure confidence in software as<br>
complex as an operating system is a pipe dream.<br>
</blockquote>
<br>
Yes, this is all true. I don't agree with you, or with him. We shall see,<br>
hopefully before I retire or drop off entirely.<br>
<br>
best wishes<br>
<br>
Paul<br>
<br>
_______________________________________________<br>
The System Safety Mailing List<br>
systemsafety@TechFak.Uni-Bielefeld.DE<br>
Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</div>
</div>
</div>
<br>
</body>
</html>