Een bordje "no hats allowed" en het is klaar.

Is dit flauw? Ach, ik moet het ze nog beter zien doen. Het is namelijk inderdaad waar dat "patch en pray" hetzelfde is als dweilen met de kraan open. En daarom uiterst lucratief voor de beveiligingsindustrie, die er een heel mythos met hoedjesdragende cyberboemannen ("hackers", die "hacken", zoals de smurfen zo smurfig smurfen) omheen gesponnen heeft om zoveel mogelijk te verbergen dat de nieuwe kleding van de keizer nog steeds vol zit met gaten.

Deze dame heeft dus door dat we dweilen met de kraan open. Joepie, werd tijd zeg. Ze is alleen vergeten dat dit "model checking"-vehikel een strikt moeilijker probleem is dan NP-complete problemen. Iedereen die tenminste een introductiecursus algorithmen gevolgd heeft weet nu dat dit nog wel even geen magische eindoplossing zal opleveren.

Waarmee niet gezegd is dat er niets is wat je kan doen. Softwareproblemen stoelen eigenlijk altijd op aannames die onterecht blijken te zijn. "Er zal nooit meer data in deze buffer gestopt worden dan er in past, dus hoeven we niet te controleren of we niet al voorbij het einde zijn", of "er zal nooit uit de inhoudsmodus gesprongen worden en dus hoeven we niet te controleren of er aanhalingstekens in de invoer zullen zitten", als twee voorbeeldjes. Meestal zijn die aannames impliciet omdat er iemand niet opgelet heeft, en dat maakt ze geniepig. Je zorgt dus dat je je aannames expliciet maakt en voordat je je er op verlaat controleer je ze. Op die manier verzeker je jezelf ervan dat alle aannames --of dan toch tenminste zoveel mogelijk-- expliciet zijn en dat je je er op kan verlaten.

Model checking zou daar best eens bij kunnen helpen, maar omdat het zelf zo'n zwaar probleem is, smijt deze dame eigenlijk vooral met buzzwords en zullen er weinig zoden aan de dijk gezet worden. Dit weten we want we zijn al een tijdje bezig met dit model checking idee, en hoewel het best leuk lijkt is het vooralsnog vooral een leuk onderzoeksspeeltje gebleken, precies omdat het zo'n hardnekkig probleem is. Waarmee in de praktijk het plaatsen van bordjes "hier geen hoedjes" best wel eens net zo effectief zou kunnen blijken te zijn.

Maargoed, dit is DARPA, en die smijten regelmatig geld naar wilde ideën of ze nou veel kans hebben of niet, want je weet maar nooit. Soms komt er inderdaad onverwacht toch iets leuks uit de bus. Zie dit dus vooral als een onderzoeksinitiatief; verwacht niet al volgend jaar over een volautomatische gatenpreventiedienst te kunnen beschikken.

Houd maar op. Ik heb al niet te hacken software.

#include <stdio.h>

void main(void) {
printf("Hello world!\n");
}

Inplaats van dan Microsoft hier aan werkt...

Compile to binary. Start hex editor and change text.... tadaa.

Zelfs IEFBR14 bleek vol met fouten te zitten, zie: http://en.wikipedia.org/wiki/IEFBR14
Het gebruik van de handig tooltje was/is alleen trigger om iets anders te activeren. Dat andere heft zijn Eigen effecten.
Doe je een compile/link voor een monolitisch programma dan komt er naast jouw code nog flink wat bij.
Bewijs maar dat de compiler de gebruikte printf functie allemaal 100% foutloos zijn. En dat dat geen gevolgen in jous programma heeft. Het is het meer een KNP probleem (graadje erger dan NP).
http://nl.wikipedia.org/wiki/NP_(complexiteitsklasse)

Heb je de headerfile geaudit? ;-)

DARPA is een van de grondleggers van het WWW, microchips en andere, (zeer) geavanceerde elektronica.
Dus als er één organisatie is, die ongelooflijke dingen voor elkaar zou kunnen krijgen, is het DARPA wel.


Maar dan ... zegt meneer de directeur ineens dit:
“What that means is there is a mathematical proof that this particular function can’t be hacked from a pathway that wasn’t intended,”
Prima, maar dat noem ik gewoon een fuzzer...

Het begint bij een formeel bewezen OS zoals http://sel4.systems/

Voor hen gold jarenlang "security was not a priority" (hun eigen woorden). Het was gewoon belangrijker snel verkoopbare rommel klaar te hebben dan om solide software te schrijven. Ze zijn er goed rijk mee geworden.

Dan moeten ze beginnen met een systeem te ontwikkelen die afzonderlijk moet draaien. Een HD met alleen het systeem erop waar geen software aan toegevoegd kan worden geen updates maar een geheel nieuw systeem elk jaar of zo. En waar andere software op een andere HD het systeem kan aanspreken om iets te doen.

Zijn dat hun eigen woorden: niet te hacken software? Ik schiet daarvan echt in een lachbui... Zolang huizen deuren moeten hebben om binnen te komen denkt het Pentagon met behoud van deze deuren het gespuis buiten te houden.
Ach neen zeg gaat iemand dat nu serieus nemen?

If I run seL4, is my system secure?
Not automatically, no. Security is a question that spans the whole system, including its human parts. An OS kernel, verified or not, does not automatically make a system secure. In fact, any system, no matter how secure, can be used in insecure ways.

However, if used correctly, seL4 provides the system architect and user with strong mechanisms to implement security policies, backed by specific security theorems.

under certain assumptions.

The brief version is: we assume that in-kernel assembly code is correct, hardware behaves correctly, in-kernel hardware management (TLB and caches) is correct, and boot code is correct. The hardware model assumes DMA to be off or to be trusted.

http://sel4.systems/FAQ/proof.pml

Als als als ;)

Correctheidsbewijzen voor software zijn heel moeilijk dus alleen bepaalde onderdelen kunnen aangepakt worden, dit zouden dan bijvoorbeeld de authenticatie functies kunnen zijn.

@ N4ppy:Ik schreef ook dat het daar begon. :) Dat is niet voor niets. ;)


DoD gaat dan ook uit van het adagium dat Confidentiality belangrijk is. De C, niet de I(integrity) en niet de A(vailability). Microsoft heeft niet voor DoD ontwikkeld.


Een harddisk is niet echt een read-only medium volgens mij. ;) Ik denk dat er aan je model nog het een en ander mankeert.

Hé een z/OS-man. Ik zoek nog werk in de z/OS tuin,want anders moet ik van de gemeente gaan schoffelen in de hunne.