F2FS Hit By Three Security Vulnerabilities: Memory Corruption, Possible Code Execution

[caligula]

there's also gonna be trashy code written for some Taiwanese webcam. In fact most code is of subpar quality.

Better development tools, expert sexchange sites, and easier languages also enable the writing of cheaper and worse quality code. We have now code written by less skilled people than ever before. The time to market for applicants has gone super low. Also people buy cheap and worse crap than ever before directly from Shenzhen.

[garegin]

Yeah. Let's take out rear view cameras, air bags and obtruction warning systems so people drive more carefully.
And btw from my experience code has gotten monumentally more complex and programs are more robust than ever. So no, application quality is not decreasing, unless your CEO is Gabe Newell.

[oiaohm]

I first heard this from 'fortune', googled it, and found the Arthur C Clarke reference, which was about software development. Handily today I can also find that on Wikipedia.

There's also this:

So close. Please note sel4 and eChronos done by data61 manage to sit right in the not possible marked area in the good fast cheep. The key is in the project management trilemma being scope. Both projects had clearly defined scope.

For a project to have a formally written scope you need documentation writers. To do formal proofs and be sure you have done everything you need a formal written scope. To make sure test cases cover everything the need to hello formal written scope useful again.

Remember sel4 and eChronos is being developed for military usage in control of weapons systems where they can in fact take someone life. The Australian military that Data61 is doing this development for does not give them a very big budget either . A weapon system being slow is not an option a slow weapon you are dead before you can fire it. Poor quality is not a option because that can kill again. So fast and good are mandatory features. Really restricted budget means cheep has to be done. So all 3 points have to be achieved as there was no other choice. This is why look into how sel4 and eChronos development is done is so interesting.

[linuxgeex]

So close. Please note sel4 and eChronos done by data61 manage to sit right in the not possible marked area in the good fast cheep. The key is in the project management trilemma being scope. Both projects had clearly defined scope.

For a project to have a formally written scope you need documentation writers. To do formal proofs and be sure you have done everything you need a formal written scope. To make sure test cases cover everything the need to hello formal written scope useful again.

Remember sel4 and eChronos is being developed for military usage in control of weapons systems where they can in fact take someone life. The Australian military that Data61 is doing this development for does not give them a very big budget either . A weapon system being slow is not an option a slow weapon you are dead before you can fire it. Poor quality is not a option because that can kill again. So fast and good are mandatory features. Really restricted budget means cheep has to be done. So all 3 points have to be achieved as there was no other choice. This is why look into how sel4 and eChronos development is done is so interesting.

It wasn't done cheap then. It was done to budget. Cheap would be half that. Then what would happen to your quality/scope/timely delivery objectives? I can promise that at 1/2 the cost you wouldn't have gotten something that matched your formal spec. You might not have even been able to afford someone to write the formal spec, or you might have written a lovely spec, then had the plug pulled on your project because it was going over (1/2 the) budget, and your product would have been vapourware. Lucky for you, nobody set an impossible budget, impossible deadline, or impossible scope.

[oiaohm]

It wasn't done cheap then. It was done to budget. Cheap would be half that. Then what would happen to your quality/scope/timely delivery objectives? I can promise that at 1/2 the cost you wouldn't have gotten something that matched your formal spec. You might not have even been able to afford someone to write the formal spec, or you might have written a lovely spec, then had the plug pulled on your project because it was going over (1/2 the) budget, and your product would have been vapourware. Lucky for you, nobody set an impossible budget, impossible deadline, or impossible scope.

Linuxgeex you have made a mistake. The formal specification of sel4 and eChronos becomes a mathematical proof. It was done under budget and way lower cost than you would expect.

https://ts.data61.csiro.au/projects/TS/l4.verified/approach.pml

The work flow is something way different to what you would expect. Yes you are correct the formal spec is not 100 percent written by human directly in sel4 and Echronos case. Quite a bit is generated. Both sel4 and eChronos worked out it about half the cost of something done cheap due to reduced debugging time.

Basically to achieve the cost level sel4 and eChronos did you have to use a different work-flow to traditional and different staff mix. You need high level mathematics person you need a documentation writer and 1/8 of the programming staff time. Why the mass reduction in programming staff time they are not wasting time going into the code working out why it not working most of the time the proof will say these lines of code are wrong and why so fix them.

Reality is you cannot get cheapest if the result is not good and fast. Impossible budget, impossible deadline, or impossible scope got to be kidding me that is exactly what those 2 projects had. For the number of lines of code at the time sel4 specification and validation was done the allocated budget was 1/20 of the normal expect cost, normal dead line for doing it was 12 months for demonstration they only got 6 months to first complete validation demonstration and it had to be absolute complete validation at 12 months. Basically if you attempt to do what sel4 or echronos has done with the method they used it is truly impossible. Over half the formal specification is generated over 90 percent of the test casing is generated sections of the final C code again generated. Basically a heck load of automation. This is Manual labour vs Automation. Reality is most of our code development is way too much manual labour and that is why you cannot achieve good fast cheep.

One of the key bits of scope to both sel4 and eChronos is the lower amount of human labour to produce final product and to release maintenance releases to keep cost as low as possible.

When something did what was called impossible it becomes a very interesting read of method to achieve it because it means they have done a method others are not doing. sel4 and eChronos did the impossible and are still doing what people say are not possible or impossible.

An implementation correctness proof between low-level design and C implementation for a code base of similar size or complexity had not been achieved before.

Even groups with 1000 times more budget and staff than what Data61 had were unable to achieve what Data61 did with sel4. Reality this was a problem that was not solved by throwing money or massive number of human hours at it instead was solved by a solid automated quality assuring development process that in it self reduces costs.

Of course scaling up what was done for sel4 to something like the Linux kernel will not be easy. Dealing with the defects that could have been detected and remove if Linux kernel had a form proof system like sel4 are not easy or cost effective either.

Really sel4 and eChronos should alter our expectations. The idea that fast, good and cheep in software development is impossible need to go away because that is demonstrated by sel4 and eChronos as false. Now it comes how can we get to where fast, good and cheep in software development is the normal.

[oiaohm]

It wasn't done cheap then. It was done to budget. Cheap would be half that. Then what would happen to your quality/scope/timely delivery objectives? I can promise that at 1/2 the cost you wouldn't have gotten something that matched your formal spec. You might not have even been able to afford someone to write the formal spec, or you might have written a lovely spec, then had the plug pulled on your project because it was going over (1/2 the) budget, and your product would have been vapourware. Lucky for you, nobody set an impossible budget, impossible deadline, or impossible scope.

Linuxgeex you have made a mistake. The formal specification of sel4 and eChronos becomes a mathematical proof. It was done under budget and way lower cost than you would expect.

https://ts.data61.csiro.au/projects/TS/l4.verified/approach.pml

The work flow is something way different to what you would expect. Yes you are correct the formal spec is not 100 percent written by human directly in sel4 and Echronos case. Quite a bit is generated. Both sel4 and eChronos worked out it about half the cost of something done cheap due to reduced debugging time.

Basically to achieve the cost level sel4 and eChronos did you have to use a different work-flow to traditional and different staff mix. You need high level mathematics person you need a documentation writer and 1/8 of the programming staff time. Why the mass reduction in programming staff time they are not wasting time going into the code working out why it not working most of the time the proof will say these lines of code are wrong and why so fix them.

Reality is you cannot get cheapest if the result is not good and fast. Impossible budget, impossible deadline, or impossible scope got to be kidding me that is exactly what those 2 projects had. For the number of lines of code at the time sel4 specification and validation was done the allocated budget was 1/20 of the normal expect cost, normal dead line for doing it was 12 months for demonstration they only got 6 months to first complete validation demonstration and it had to be absolute complete validation at 12 months. Basically if you attempt to do what sel4 or echronos has done with the method they used it is truly impossible. Over half the formal specification is generated over 90 percent of the test casing is generated sections of the final C code again generated. Basically a heck load of automation. This is Manual labour vs Automation. Reality is most of our code development is way too much manual labour and that is why you cannot achieve good fast cheep.

One of the key bits of scope to both sel4 and eChronos is the lower amount of human labour to produce final product and to release maintenance releases to keep cost as low as possible.

When something did what was called impossible it becomes a very interesting read of method to achieve it because it means they have done a method others are not doing. sel4 and eChronos did the impossible and are still doing what people say are not possible or impossible.

An implementation correctness proof between low-level design and C implementation for a code base of similar size or complexity had not been achieved before.

Even groups with 1000 times more budget and staff than what Data61 had were unable to achieve what Data61 did with sel4. Reality this was a problem that was not solved by throwing money or massive number of human hours at it instead was solved by a solid automated quality assuring development process that in it self reduces costs.

Of course scaling up what was done for sel4 to something like the Linux kernel will not be easy. Dealing with the defects that could have been detected and remove if Linux kernel had a form proof system like sel4 are not easy or cost effective either.

Really sel4 and eChronos should alter our expectations. The idea that fast, good and cheep in software development is impossible need to go away because that is demonstrated by sel4 and eChronos as false. Now it comes how can we get to where fast, good and cheep in software development is the normal. Fast good cheep does not require leaving C as both sel4 and eChronos are both written in C with executable proof written in haskell. So limited new programming languages as well.

[oiaohm]

It wasn't done cheap then. It was done to budget. Cheap would be half that. Then what would happen to your quality/scope/timely delivery objectives? I can promise that at 1/2 the cost you wouldn't have gotten something that matched your formal spec. You might not have even been able to afford someone to write the formal spec, or you might have written a lovely spec, then had the plug pulled on your project because it was going over (1/2 the) budget, and your product would have been vapourware. Lucky for you, nobody set an impossible budget, impossible deadline, or impossible scope.

https://ts.data61.csiro.au/projects/TS/l4.verified/approach.pml

The work flow is way different. To achieve good fast cheep you do not have a workflow where any part is isolated from each other.
<b>An implementation correctness proof between low-level design and C implementation for a code base of similar size or complexity had not been achieved before.</b>
The scope was impossible before they did it. So yes Australian mil was insane enough to request the impossible with budget, deadline and scope.

The difference here is automation. Automated quality control with automated proof checking reduces you defects and reduced the labour you need to deal with them to get product to somewhat usable. So cheap it is. Cheap without automated validation/proof ends up costing more than cheep with. Of course this also means you have fast and good.