CompCert specified a language called Verified C. It is implemented by their compiler in the Verified Software Toolchain. It is all explained on their website.
Good. I approve. But until it's there, I can provide quality controls in C that aren't in Rust.
I absolutely applaud bringing Rust to the formal methods table. They talk of unsafe Rust and there's only one way to find out if any given Rust is unsafe (unless it's something trivial like a dangerous instruction).
Until there is hard evidence as to what actually is unsafe, in terms of more complex constructs, arguments over language safety are speculative.
I actually use Rust (and C and Ada, Occam, Java...) but I am very careful over boasts. I might well help out the project you mentioned.
It shouldn't be hard to make CPN Tools output Rust code, and then you could design state machines, but not sure if that would be accepted. It would still be helpful.
The problem with such a solution, indeed the problem with safe programming in general, is that it has to be documented. You obviously knew how to explain it and were meticulous. That's good. And rare.
Too many are taught to hate properly documenting or explaining their code, with the result that you've unmaintainable code. They're also taught to hate designing and testing, with the same result.
In industry, programmers are often banned from performing all four key tasks because of deadlines and the manager wanting to look good.
I was taught many of the rules that were eventually compiled into NASA's Power of Ten, which I'd consider a minimal set of principles, but neither schools nor industry emphasize or enforce code quality.
And now you're going to compare them against SEL4, FreeRTOS, Linux and OpenBSD?
No comparison on defect density, security, performance and features means that for all we know those choices you offer are toys. You don't have to produce the comparison, a link is fine. Someone has to have shown that these OS' are worth it.
There are things in C11 that are missing in Verified C.
There are things in C11 you are advised against using under the CERT Secure Programming standards, MISRA and JSF.
Most of the tasks can still be done, they just have to be done differently, which is why the trade-off is only limited. If you can still solve the problem, just with different syntax, then the trade-off is not in capability but in expediency. That just requires a library of helper routines and I'm sure you can find those.
So you're saying the authors of SEL4 chose the wrong language or paid attention to the wrong details?
Fine. Using their abstract theorems as your starting point, write an OS in, say, Rust or Nim that has equal or superior performance that complies with the same theorems.
If you can't, or the man-hours effort required would match or exceed those expended by the developers on the code alone, then I postulate they paid attention to the right details.
That's why we have NASA's Power of Ten, formal methods, coloured Petri nets, implementing to test harnesses, mock objects, FRAMA-C, Why3, Verified C and documentation.
Programmers can use one or more of these, to develop code that's as good as they want it to be. You don't have to use all of those methods, proper use of any one would suffice in many cases.
Programmers are either psychologically primed, through inept schooling or hostile management, to avoid these. Schooling and management aren't affected by the language you choose. If they're unfit for purpose, they'll remain so whatever the language.
Can't do much about schools people have finished with, but management is another matter. Bad management can be disciplined. Individually, we can't pull a Feynman, we have to start thinking a bit more collectively.
As long as we squabble like rats, managers will treat us like rats and the code will look like it's a nest for rats.
Already used in operating systems, so we know it's powerful enough.
Verified C has three important features, of which two cover the issues from the original article.
First, it eliminates the ambiguities, although the current C specification has very few left.
Second, it is possible to guarantee correctness. Technically, this has been true for any C dialect for some time, provided you avoid ambiguous constructs, but this is easier.
The third feature, probably of greatest interest to embedded developers, is that the binaries can be proven to match the source in behaviour.
Because it is a dialect of C, with a known ABI, GCC will compile the code - sans the binary proof. Further, ld should be easily coaxed into linking VST-compiled kernel code with GCC-compiled code if it can't already.
So, if we went this route, we keep everything in C, we simply modify the more critical functions to use the Verified C dialect. Everything compiles as it did before, behaves as it did before, but we can now use formal methods to examine those functions.
Because you can use GCC, there's no risk of a performance hit although Verified C is said to be comparable to GCC.
Because we can do this one function at a time, you're not looking at a kernel rewrite but a normal-sized patch with each development cycle.
Just as security only requires a security kernel to be correct, you don't need to do safety checking over the kernel. So this approach needs only a tiny number of functions verified.
Is this the best solution? I don't know, but it's a proof that C can be made as safe as you like without impacting speed or functionality.
An alternative approach is for the Big Three (Red Hat, SuSE and Ubuntu) to agree to jointly fund two projects - one to properly document Linux internals, and one to properly test the hell out of it.
The cost would be peanuts to them, but systematic testing and systematic documentation would make finding and fixing bugs a lot easier. It isn't C that's the problem, it's digging around in C in the dark.
Is Rust less dangerous than Verified C Dr the Verified Software Toolchain? Do I have anything equivalent to Why3 to verify correctness?
The kernel, in C, can have critical components modified to fit the constraints. It's still C, GCC will still compile it, but I could then verify it. Without impacting performance.
Linux is big, if you want to convince me you cod write an OS kernel in Rust (remember, no standard libraries), start with rewriting SEL4. Whilst retaining or improving on the defect ratio and performance.
If you can't do something that small, you can't do Linux.
I understand the role of the FCC. I understand its regulations and I understand how its role with the Internet has changed. I've read its rules and regulations. Have you?
Ummm, you might be interested to learn I've been using, not playing, with the Internet since the mid 1980s, have built one international hub and been employed by another, and have actively worked with the IETF.
In other words, that four digit UID isn't bought. Show respect for your elders, we might have learned things over the years.
If you do not understand the posts of those who have been there, done that, ASK. DONT ASSUME you are all wise. If you do not understand, that is YOUR failure. Fix it.
I'm able to state that the senior officials and firemen involved have all stated this to be part of the contract. If you wanted to know, you'd be asking them. Asking me suggests you'd rather not know. I'm curious as to why. Because then you'd be faced with an incontrovertible fact that you'd been lied to?
That happens. It's better to find out the truth even if it means corporations do bad things to good people and that libertarian philosophy doesn't work in a monoculture.
Prior to Busy declaring data carriers weren't telecos, by exec order, the Internet was protected against such malign behaviour. After Obama reinstated the above, the Internet was protected.
In the few years between? There were problems. That's just historical fact.
They were on a corporate plan with a specific emergency clause that stated that in a declared emergency, Verizon promised not to throttle.
Verizon broke contract.
This should be end of story, but apparently there's a lot of support for the idea that contracts have no standing. If this reaches SCOTUS and is confirmed, contract law will be nullified.
It's common knowledge the plan they had specifically included a clause for no throttling in emergencies. The discussion is over whether Verizon can lawfully break contractual clauses because they feel like it, and if so which ones.
Currently, the FCC and Federal government are inclined to the view that contractual clauses are irrelevant. The courts are undecided. If the courts do decide contracts have no legal standing, that could have some I interesting consequences.
That's the rule in the U.S., except they never check if the company has any intention of delivering. Hence the massive overruns, failed projects, etc. Ditto for the UK.
This debate was held in the 70s and 80s. In Reagan's time, it was well established that data was regulated the same as voice, that ISPs were telecos no different from any other.
This was settled until Bush passed an executive order nullifying this. You cannot change the law with an executive order. Bush classed data as distinct, by order.
If you want to talk Congress, fine, but start with eliminating Bush's order and THEN talk Congress.
Slashdot Mirror
CompCert specified a language called Verified C. It is implemented by their compiler in the Verified Software Toolchain. It is all explained on their website.
Good. I approve. But until it's there, I can provide quality controls in C that aren't in Rust.
I absolutely applaud bringing Rust to the formal methods table. They talk of unsafe Rust and there's only one way to find out if any given Rust is unsafe (unless it's something trivial like a dangerous instruction).
Until there is hard evidence as to what actually is unsafe, in terms of more complex constructs, arguments over language safety are speculative.
I actually use Rust (and C and Ada, Occam, Java...) but I am very careful over boasts. I might well help out the project you mentioned.
It shouldn't be hard to make CPN Tools output Rust code, and then you could design state machines, but not sure if that would be accepted. It would still be helpful.
Formal methods are needed to provide sanity in any language. Don't leave home without them.
Z is as much a mainstay of the Ada community as the C community.
Verified C has less syntax than C11.
So I'm unsure what you're referring to.
Youngsters!
The problem with such a solution, indeed the problem with safe programming in general, is that it has to be documented. You obviously knew how to explain it and were meticulous. That's good. And rare.
Too many are taught to hate properly documenting or explaining their code, with the result that you've unmaintainable code. They're also taught to hate designing and testing, with the same result.
In industry, programmers are often banned from performing all four key tasks because of deadlines and the manager wanting to look good.
+6 Insightful.
I was taught many of the rules that were eventually compiled into NASA's Power of Ten, which I'd consider a minimal set of principles, but neither schools nor industry emphasize or enforce code quality.
And now you're going to compare them against SEL4, FreeRTOS, Linux and OpenBSD?
No comparison on defect density, security, performance and features means that for all we know those choices you offer are toys. You don't have to produce the comparison, a link is fine. Someone has to have shown that these OS' are worth it.
Strict type checking isn't all bad, as long as the code is properly designed and you write the test procedures first.
The problem is that schools and industry discourage testing, minimalize it and place it last - usually after deployment. As for design... hah!
I see limited evidence of a trade-off.
There are things in C11 that are missing in Verified C.
There are things in C11 you are advised against using under the CERT Secure Programming standards, MISRA and JSF.
Most of the tasks can still be done, they just have to be done differently, which is why the trade-off is only limited. If you can still solve the problem, just with different syntax, then the trade-off is not in capability but in expediency. That just requires a library of helper routines and I'm sure you can find those.
So you're saying the authors of SEL4 chose the wrong language or paid attention to the wrong details?
Fine. Using their abstract theorems as your starting point, write an OS in, say, Rust or Nim that has equal or superior performance that complies with the same theorems.
If you can't, or the man-hours effort required would match or exceed those expended by the developers on the code alone, then I postulate they paid attention to the right details.
Ada is interesting, as is Spark (the secure subset). What do you think of Eiffel?
I am trying to get Occam-Pi working. Had no luck tracking down Guppy, Occam's successor. That, too, has a place in the world.
That's why we have NASA's Power of Ten, formal methods, coloured Petri nets, implementing to test harnesses, mock objects, FRAMA-C, Why3, Verified C and documentation.
Programmers can use one or more of these, to develop code that's as good as they want it to be. You don't have to use all of those methods, proper use of any one would suffice in many cases.
Programmers are either psychologically primed, through inept schooling or hostile management, to avoid these. Schooling and management aren't affected by the language you choose. If they're unfit for purpose, they'll remain so whatever the language.
Can't do much about schools people have finished with, but management is another matter. Bad management can be disciplined. Individually, we can't pull a Feynman, we have to start thinking a bit more collectively.
As long as we squabble like rats, managers will treat us like rats and the code will look like it's a nest for rats.
Then how come I can use formal methods with C (the ultimate test of correctness) but not Rust?
The developers of FRAMA-C, the Verified Software Toolchain and the SEL4 operating system disagree.
Why should I take your word over the experts?
Spark (a subset of Ada for mission-critical work) would seem better, given that safety is apparent the concern.
I say apparently as I see no evidence safety is of interest at all.
Already used in operating systems, so we know it's powerful enough.
Verified C has three important features, of which two cover the issues from the original article.
First, it eliminates the ambiguities, although the current C specification has very few left.
Second, it is possible to guarantee correctness. Technically, this has been true for any C dialect for some time, provided you avoid ambiguous constructs, but this is easier.
The third feature, probably of greatest interest to embedded developers, is that the binaries can be proven to match the source in behaviour.
Because it is a dialect of C, with a known ABI, GCC will compile the code - sans the binary proof. Further, ld should be easily coaxed into linking VST-compiled kernel code with GCC-compiled code if it can't already.
So, if we went this route, we keep everything in C, we simply modify the more critical functions to use the Verified C dialect. Everything compiles as it did before, behaves as it did before, but we can now use formal methods to examine those functions.
Because you can use GCC, there's no risk of a performance hit although Verified C is said to be comparable to GCC.
Because we can do this one function at a time, you're not looking at a kernel rewrite but a normal-sized patch with each development cycle.
Just as security only requires a security kernel to be correct, you don't need to do safety checking over the kernel. So this approach needs only a tiny number of functions verified.
Is this the best solution? I don't know, but it's a proof that C can be made as safe as you like without impacting speed or functionality.
An alternative approach is for the Big Three (Red Hat, SuSE and Ubuntu) to agree to jointly fund two projects - one to properly document Linux internals, and one to properly test the hell out of it.
The cost would be peanuts to them, but systematic testing and systematic documentation would make finding and fixing bugs a lot easier. It isn't C that's the problem, it's digging around in C in the dark.
Is Rust less dangerous than Verified C Dr the Verified Software Toolchain?
Do I have anything equivalent to Why3 to verify correctness?
The kernel, in C, can have critical components modified to fit the constraints. It's still C, GCC will still compile it, but I could then verify it. Without impacting performance.
Linux is big, if you want to convince me you cod write an OS kernel in Rust (remember, no standard libraries), start with rewriting SEL4. Whilst retaining or improving on the defect ratio and performance.
If you can't do something that small, you can't do Linux.
I understand the role of the FCC. I understand its regulations and I understand how its role with the Internet has changed. I've read its rules and regulations. Have you?
Ummm, you might be interested to learn I've been using, not playing, with the Internet since the mid 1980s, have built one international hub and been employed by another, and have actively worked with the IETF.
In other words, that four digit UID isn't bought. Show respect for your elders, we might have learned things over the years.
If you do not understand the posts of those who have been there, done that, ASK. DONT ASSUME you are all wise. If you do not understand, that is YOUR failure. Fix it.
Verizon is a telecommunications provider. The laws governing what a teleco can do to a pipe IS FCC business.
I'm able to state that the senior officials and firemen involved have all stated this to be part of the contract. If you wanted to know, you'd be asking them. Asking me suggests you'd rather not know. I'm curious as to why. Because then you'd be faced with an incontrovertible fact that you'd been lied to?
That happens. It's better to find out the truth even if it means corporations do bad things to good people and that libertarian philosophy doesn't work in a monoculture.
No, peer-to-peer agreements for tier 1 prevent that.
Well, they did. They don't, now.
Prior to Busy declaring data carriers weren't telecos, by exec order, the Internet was protected against such malign behaviour. After Obama reinstated the above, the Internet was protected.
In the few years between? There were problems. That's just historical fact.
They were on a corporate plan with a specific emergency clause that stated that in a declared emergency, Verizon promised not to throttle.
Verizon broke contract.
This should be end of story, but apparently there's a lot of support for the idea that contracts have no standing. If this reaches SCOTUS and is confirmed, contract law will be nullified.
You sure that's a good idea?
They did negotiate another plan.
It's common knowledge the plan they had specifically included a clause for no throttling in emergencies. The discussion is over whether Verizon can lawfully break contractual clauses because they feel like it, and if so which ones.
Currently, the FCC and Federal government are inclined to the view that contractual clauses are irrelevant. The courts are undecided. If the courts do decide contracts have no legal standing, that could have some I interesting consequences.
That's the rule in the U.S., except they never check if the company has any intention of delivering. Hence the massive overruns, failed projects, etc. Ditto for the UK.
This debate was held in the 70s and 80s. In Reagan's time, it was well established that data was regulated the same as voice, that ISPs were telecos no different from any other.
This was settled until Bush passed an executive order nullifying this. You cannot change the law with an executive order. Bush classed data as distinct, by order.
If you want to talk Congress, fine, but start with eliminating Bush's order and THEN talk Congress.