Erstaunliche Summen stehen da im Raum 50 000 Dollar für eine Woche. Wenn das nicht bemerkenswert ist…., muß denjenigen die sei Jahren keinen Urlaub bekamen und vielleicht 15 000 Dollar im Jahr verdienen runtergehen wie Öl….

Aber klar wer in Billionen rechnet wird wohl bei ein paar Zehntausendern wohl kaum “verzweifeln”

Es heißt ja, die Zeit heilt alle Wunden. Bei vielen Sachen würde ich dem zustimmen aber manche Sachen “heilen” nie, sie werden nur überdeckt und bei einem kleinen Anlaß kommen Sie wieder hoch. Ich denke man kann es als “unbeabsichtigtes behalten” beschreiben, was einem da manchmal in die Quere kommt.

Tenor, unsere tollen Politiker haben das “System” gerettet. Nun ja nachdem Sie es mit zugrunde richteten. Nur zu was für einen Preis. Ich hätte lieber die Politiker untergehen sehen nund brüsten Sie sich mit fremden Federn lies meinem Geld. Allerdings bedarf es schon einer besonderen Chuzpe zu behaupten zur Rettung der HRE hätte es keine Alternative gegeben. Das ist definitv gelogen. Und irgendwann wird sich dieser auf Kredit aufgebaute Staat nicht mehr mit noch mehr Kredit retten können.

Diese unsägliche Ab(fuck)wrack prämie läuft aus. Nun schauen wir mal auf die Auswirkungen
1) Offentsichtlich konnten mehr kleine Autos verkauftt werden
2) Offensichtlich wurde der Gebrauchtwagenmarkt kaputt gemacht
3) Offentsichtlich wurde kleinen Autoreparaturbetrieben massiv Geschäft entzogen
4) Offentsichtlich wurden viele Autoverkäufe “vorgezogen”

Also wir haben Autohersteller und deren Leute subventioniert und nun läuft diese Well aus. Was das bedeutet ist klar. Nächtes Jahr wird es bei den Autoherstellern noch finsterer….

Der Gebrauchtmarkt für alte aber immer noch solchen mit besseren Abgaswerten wurden den Entwicklungsmärkten entzogen. Also müssen die alten Dreckschleudern noch länger fahren. Da bei uns der Markt doch eher gesättigt ist dürfte es also im Großen und Ganzen in den Entwicklungsländern weitaus mehr Autoverkäufe geben als bei uns. Nur das wurde den Leuten ja gestohlen. Reparaturen wurden nicht mehr vorgenommen und wertvolle Rohstoffe sinnlos vernichtet. Ein “toller” Erfolg. Mal sehen wie es die Politiker nächstes Jahr oder nach der Wahl drehen werden.

Weitaus schlimmer: Offenbar wurden viele Autos auf Pump gekauft, d.h für diese Wagen wurden Schulden gemacht. Offensichtlich ist es unseren Politikern nicht aufgefallen, daß zuviele Schulden durch noch mehr Schulden kuriert werden sollen. Ergo wir werden wohl im nächsten Jahr weitaus mehr Privatinsolvenzen “erleben”

Wirklich eine gelungenes Beispiel, wie bescheiden der Staat in der Wirtschaft darsteht. Das bescheiden dürfen sie ruhig verschärfen….

There is an announcement of a first formal proof of a kernel written in C

However just see those figures:
“The outcome is the result of four years’ research by Dr Klein’s team of 12 NICTA researchers, NICTA/UNSW PhD students and UNSW contributed staff. They have successfully verified 7,500 lines of C code and proved over 10,000 intermediate theorems in over 200,000 lines of formal proof. The proof is machine-checked using the interactive theorem-proving program Isabelle. It is one of the largest machine-checked proofs ever done.”

Four years for “just 7500 lines of C and just see what they’ve done for the proofs, (who the hell will verify 200 000 lines of formals proofs) however if that is what it takes then we have a ratio of
roughly 1/200. That means for a code base of around 1 000 000 lines we would have to accept 200 000 000 lines of proof, not reagarding the exponential grows of proababilty. But let us just assume a linear scale than this would take around 133,33 years to build the proof. Now that’s really quite a time if we just let IT to be around 60 years or so old…..

Just another point:
The proof is machine-checked using the interactive theorem-proving program Isabelle.

So who guarantees that Isabelle does get it right?

And one other figure let us assume that one does can write around 30 Lines of code an hour, than one needs around 7500 / 30 250 hours to write 7500 lines. That just a bit below 6 weeks. Let us assume 200 EUR for payments then this would be around 200 * 250 = 50 000. Now the proof has taken 4 years let us assume one person could have done it in that time so we have around 250 * 8 = 2000 hours a year so for four years that arou around 8000 hours now let’s do one other calculation, the “proof” has costed 8000 * 200 = 1 600 000 EUR.

Just imagine, you spend that much money on the assumption you get it all right, and then just see what they wrote:
“The proof also shows that many kinds of common attacks will not work on the seL4 kernel. For instance, the microkernel is impervious to buffer overflows, a common form of software attack where hackers take control of programs by injecting malicious code. “Our seL4 kernel cannot be subverted by this kind of attack,” says Dr Klein.”

How cost effective would it have been to use a language which does not even permit this buffer overflows and just see how expensive those buffer overflows really are….

This is an amazing number.

However the conclusions are very doubtful:
“The NICTA team has achieved a landmark result which will change the game for security-
and safety-critical software,” said OK Labs’ Chief Technology Officer and Leader of NICTA’s
ERTOS Group, Professor Gernot Heiser. “It provides conclusive evidence that bug-free
software is possible, and in the future nothing less should be considered acceptable where
critical assets are at stake. OK Labs looks forward to taking this groundbreaking research to
market.”

This has simply a touch of lying. The conculsion is simply wrong, what will happen if the program still has some bug? What will they tell us then, “well sorry but we have a fault in lined 179333 of our “formal proof”.”

Another point about the “kernel”
“The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commercialisation activities, and thus is currently proprietary. We are endeavouring to release seL4 in the future, but the time-line and exact nature of the release is yet to be decided. Stay tuned for further info.”
see here:http://ertos.nicta.com.au/research/sel4/

So the kernel is not available at all and sorry, it has not run under “real” scenarios. And it was written by the same group. Sorry, that has a bit more than just a small smell.

Let’s see if the stuff ever will hit the market and how it will “survive” in the wild. Maybe we just read about it in a few other articles but never see it in reality….

Was für eine Logik kann dahinter stecken. Da verschwenden die Politiker Milliarden, in dem die “den armen Banken” das Geld nur so hinterherwerfen, und keiner schreibt was. Selbst die Journalisten beschreien die Politker als “Heiler”. Und dann so eine Well wegen eines Mercedes der mal eben 2000 km fahren muß? Da wird auf einmal der Untergang des Abendlandes beschrieen?

Wie schmerzfrei muß man denn da sein?

Nu’ is’ses raus. Banken in Schwierigkeiten sollten nicht mehr Pleite gehen sondern “politisch” verwaltet werden. Das ist die neuests “tolle” Idee von unserem Wirtschaftsminister. Oh ja, wie gut das funktioniert kann man an den Landesbanken sehen. Und wie immer fällt unter den Tisch wer die meisten Miesen gemacht hat. Hallo Politiker, Ihr seid es…

Satire? Mit Sicherheit
Real? leider allzu