Experimental Patches For Rust-Written Linux Network Drivers

[Nth_man]

> Sound static analysis [...] is far more interesting because the results are as reliable as mathematical proofs.
-- https://sws.cs.ut.ee/Thesis/SoundAnalysis

So is Rust's borrow checker.

Do you have any reference for that?

> > Reading https://nvlpubs.nist.gov/nistpubs/ir...ST.IR.8304.pdf , some sound static analyzers can check Motor Industry Software Reliability Association (MISRA) guidelines, when human lives are at risk...

> And we all know as a result there are no recalls because of software issues in the automotive industry, right? Static analyzers are that good.

"can check" doesn't mean "are utilized to check". MISRA guidelines, sound static analyzers (different from the ones which are not sound), etc. are not used in every software in the automotive industry.

[bug77]

Do you have any reference for that?

https://plv.mpi-sws.org/rustbelt/stacked-borrows/paper.pdf

You can also ask ChatGPT

> > Reading https://nvlpubs.nist.gov/nistpubs/ir...ST.IR.8304.pdf , some sound static analyzers can check Motor Industry Software Reliability Association (MISRA) guidelines, when human lives are at risk...

> And we all know as a result there are no recalls because of software issues in the automotive industry, right? Static analyzers are that good.

"can check" doesn't mean "are utilized to check". MISRA guidelines, sound static analyzers (different from the ones which are not sound), etc. are not used in every software in the automotive industry.

So... a tool that might be used, but it's not really used, except for some very, very specific apps is as good (or better) than a compiler that verifies things at every compile, now way around it? Is that what you're telling me?

[Nth_man]

> > > Sound static analysis [...] is far more interesting because the results are as reliable as mathematical proofs.
> > > -- https://sws.cs.ut.ee/Thesis/SoundAnalysis

> > So is Rust's borrow checker.

> Do you have any reference for that?

https://plv.mpi-sws.org/rustbelt/stacked-borrows/paper.pdf

Mmm... it's not written there that using that borrow checker the results are as reliable as mathematical proofs (as written by the aforementioned university). The NIST report on Dramatically Reducing Software Vulnerabilities emphasizes the need for sound analysis and explains the distinction neatly: "Heuristic analysis is faster than sound analysis, but lacks assurance that comes from a chain of logical reasoning".

> You can also ask ChatGPT

Doesn't look like a good idea

> So... a tool that might be used, but it's not really used, except for some very, very specific apps

Mainly when human lives are at risk: nuclear, aerospace...

> is as good (or better) than a compiler that verifies things at every compile, now way around it? Is that what you're telling me?

"Safety-critical embedded software has to satisfy stringent quality requirements. One such requirement, imposed by all contemporary safety standards, is that no critical run-time errors must occur. Runtime errors can be caused by undefined or unspecified behavior of the programming language; examples are buffer overflows or data races. They may cause erroneous or erratic behavior, induce system failures, and constitute security vulnerabilities.

A sound static analyzer reports all such defects in the code, or proves their absence. Sound static program analysis is a verification technique recommended by ISO/FDIS 26262 for software unit verification and for the verification of software integration". [...] The experimental results confirm that sound static analysis can be successfully applied for integration verification of large-scale automotive software. [...]
-- https://www.sae.org/publications/tec.../2019-01-1246/
-- https://doi.org/10.4271/2019-01-1246

[Nth_man]

And as Phoronix usually does, a post with five links gets an "Unapproved" label. We'll wait until it gets "approved"...

[bug77]

Mmm... it's not written there that using that borrow checker the results are as reliable as mathematical proofs (as written by the aforementioned university). The NIST report on Dramatically Reducing Software Vulnerabilities emphasizes the need for sound analysis and explains the distinction neatly: "Heuristic analysis is faster than sound analysis, but lacks assurance that comes from a chain of logical reasoning".

That's exactly what is says, it's just worded differently.

> You can also ask ChatGPT

Doesn't look like a good idea

Yeah, it explains better than I can and you can't really argue with it. Sorry, I didn't think it through.

> So... a tool that might be used, but it's not really used, except for some very, very specific apps

Mainly when human lives are at risk: nuclear, aerospace...

> is as good (or better) than a compiler that verifies things at every compile, now way around it? Is that what you're telling me?

"Safety-critical embedded software has to satisfy stringent quality requirements. One such requirement, imposed by all contemporary safety standards, is that no critical run-time errors must occur. Runtime errors can be caused by undefined or unspecified behavior of the programming language; examples are buffer overflows or data races. They may cause erroneous or erratic behavior, induce system failures, and constitute security vulnerabilities.

A sound static analyzer reports all such defects in the code, or proves their absence. Sound static program analysis is a verification technique recommended by ISO/FDIS 26262 for software unit verification and for the verification of software integration". [...] The experimental results confirm that sound static analysis can be successfully applied for integration verification of large-scale automotive software. [...]
-- https://www.sae.org/publications/tec.../2019-01-1246/
-- https://doi.org/10.4271/2019-01-1246

What can I say... I hope you're not using commodity CPUs either. I hope you're exclusively running CPUs that work in nuclear power plants and the ISS, because the others aren't radiation-hardened, this totally on a totally unacceptable safety level.

[Nth_man]

> That's exactly what is says, it's just worded differently.

Can you tell where?

[piotrj3]

Can you tell where?

https://hal.science/hal-01633165v2/document

Chapter 7 called "7PROOF OF SOUNDNESS"

In particular, the adequacy theorem guarantees that a semantically well-typed program is memory
and thread safe: It will never perform any invalid memory access and will not have data races.
Put together, these theorems establish that,if the only code in aλRustprogram that is not syntacti-
cally well-typed appears in semantically well-typed libraries, then the program is safe to execute.

This paper covers quite a lot of types, mutexes, thread safety etc. and proofs concept of ownership/borrowing/memory is safe in Rust.

Also github considers soundness breaking serious in case of Rust and there is/was special label even on github to track those and they are considered high priority bugs most of time. They of course exist (LLVM, impelementations of models aren't perfect even if model was perfect and this applys to stuff like astree/spark/frama-c/misra-c.

[Nth_man]

> > So is Rust's borrow checker.

> Do you have any reference for that?

https://hal.science/hal-01633165v2/document

Chapter 7 called "7PROOF OF SOUNDNESS"

In particular, the adequacy theorem guarantees that a semantically well-typed program is memory
and thread safe: It will never perform any invalid memory access and will not have data races.
Put together, these theorems establish that,if the only code in aλRustprogram that is not syntacti-
cally well-typed appears in semantically well-typed libraries, then the program is safe to execute.

We can read that in that paper, although how do we know it's a "semantically well-typed program"? (different from a "syntactically well-typed program"). Borrow checkers can not solve that.

[piotrj3]

We can read that in that paper, although how do we know it's a "semantically well-typed program"? (different from a "syntactically well-typed program"). Borrow checkers can not solve that.

Borrow-checker in Rust is one piece of puzzle. Rust really strong typing system is another.

Paper defines what is semantically well-typed program + refers few papers with same definition. Paper also mentions that such proof is very rare and somehow none of papers mentioned refer to astree or spark or any language of this type.

But about papers:
- they talk about subset of Rust. Why subset - because whole language would be impossible (even godel's incompletness theorem for sure would appear there), in fact SPARK, frama-C, misra-C all use subset of languages they come from (Ada and C). This is very important - formally proving entire language safety would be probably impossible and sure someone could find couterexample of that something cannot be proven, however both papers use realistic subsets.
- they make a formal model that is similar/matching model of Rust, implement own tooling and that tooling found real bugs in Rust. They didn't prove however failure of model. So now Rust have some formal verification tools like Mira (that uses stackedborrows from paper Bug77 sent) and not only this tool makes sure Rust is safer implementation wise including unsafe usage, this tool keeps expanding for such errors.
- most tools/languages we talk about is formally verified only on model level. They do not tell you for example implementation of compiler is formally correct, or implementation of sound verification tools is formally correct and catches all issues. There are ways to ensure higher quality of those (AdaCore - creator of SPARK toolchain has an ISO 26262 and IEC 61508 qualification for example), but sound verification doesn't prove true absence of bugs, Rust relies on OS (as everyone), Rust relies on LLVM (we have to rely on LLVM or gcc anyway), we cannot prove those are safe - ever probably.

My favourite example is WPA2. WPA2 entire protocol of exchanging keys was mathematically proven to be safe. Entire security of WPA2 was proven. WPA2-KRACK attack happened and said hello - an error that came for lack of foresight in standard itself.

Soundness proof is also rather weak proof. Except of security attacks I already mentioned that soundness takes absolutly 0 care of - the problem in for example aerospace industry is way bigger - you fly high, a lot of SPARK clients are in space literally and you are bombared by cosmic rays - so you need redundancy calculation + all types of ECC memory etc. Soundness does nothing. Soundness cannot prove you safety on barriers user mode-kernel mode or interactions between programs or interactions between program and hardware. Soundness doesn't take care of issues of sort - hey we are far in sky, our pressure sensor died and shows we have 0 pressure so airplane now thinks we are 1 milion feet in sky so it decided to automatically nose dive. Soundness on level of code doesn't also do much, you also need to prove after all transformations compiler do, soundness is retained post transformation of code. Spark having more enforced compiler and having option to custom verification definition spec allows you to properly match those requirements.

Thing is Rust is way more realistic language to use widely (you are allowed to do a lot more stuff) then Spark/frama-c/misra-c/astree C and provides good enough safety to use it. SPARK to for example do illegal stuff, simply goes into ADA mode.

[rogerx]

> You can also ask ChatGPT

Thought my questions and concerns with Rust language and systemd were already being responded by ChatGPT here.