ab praeceptis • November 19, 2016 7:20 AM

Nick P, Clive, Thoth (et al.)

I did a little digging on kaspersky os.
The russian wikipedia article didn’t tell a lot but contained hints that put me on the trace.

They are partnering with sysgo, the guys who commerzialized the fiasco microkernel (and the kaspersky thingy just so happens to support exactly the same architectures). They are talking about verifiability and about verifiable code.
And they have learned some tricks from some others like, for instance, minix 3.

All in all we’re talking, it seems, about yet another L4 based approach (to avoid using the term “copy”), possibly based on seL4 with some resilience à la Minix 3 thrown in and some hash or signature magic (I personally tend to think it’s hashes).

I’m somewhat split. For a start it’s certainly not a secure OS (unless compared to ubuntu) but that’s not my issue. What I mean is that it’s not secure as, for instance Nick P. or Clive or myself would define that. But I think that a considerably more safe OS than the common wide spread ones (like linux 2.6 in plastic boxes) actually is quite some progress and damn good enough for many low to mid level scenarios. So that’s not my issue.

Looking at kaspersky os from that angle, yes it certainly has some value and can make bazillions of infrastructure boxes much more secure than the usual linux crapware.

What strongly disturbs me, though, is that from what I see so far kaspersky OS is just a “get/buy some blocks and then use your big name and marketing power” product. Frankly, I take kaspersky os to be more of a quick $ marketing hype rip-off than a serious contender in its field.

I’m under the impression that the driving force in kasperkys thinking was not security but that he had that marketing idea and as soon as all the major blocks were available (seL4, Minix3, some “code verifiers”) he just mangled those blocks together, added some magic sauce – based on consumer impressing buzzwords, not on real security – like “signatures” that can only be broken by Q (so he says), and started his sales tour.

From what very little code I saw, unlike Joe or Jane, I’m not at all impressed. First it’s C (and quite probably C++ on some higher layers). That’s a very strong counter-indication. Next and more importantly I saw but some typedefs – but no functions.
I may be wrong but to me that tells something. That tells me that he is avoiding to actually show anything that would allow at least a guesstimate of their real approach; they are mereley targetting Joe and Jane and brain-dead golden sticker driven middle management.

Why am I saying that? Because with a function I could see ACSL or at least Deputy/Ivy annotations (if they existed). With typedefs I can’t. All I could see is that his coders seem to be disciplined. So what, that’s non-news in Russia.

But he talks about “verified” and “verifiable”. My take: marketing blabla.

His “verification” is – at best – running his stuff through clangs static analyzer (which is but a funny modestly useful toy as of now). That’s laudable for the average C developer drone working on, say, some gui code, but in the context of verifiable security it’s ridiculous.
There is a very simple law: If you use C/C++ (which you should not do in areas like a secure os) then you damn use ACSL/Frama-C or sep.logic/verifast (which is much harder to do). Everything else is not acceptable. Simple as that.

Well noted, I’m not in any way anti-kaspersky. From what I know they make some good products (well, as far as AV can be a good product) but this kasperky os is IMO little more than marketing hype. Kaspersky certainly knows how to make a ton of money but I see no reason to believe he also knows to create a safe and secure operating system.

Sorry. 4 out of 10 is the best I can offer for that attempt.

ab praeceptis • November 19, 2016 2:59 PM

Nick P.

Maybe I got you wrong but if you are really smirking at Provencore you are mistaken I think.

For a start, they don’t play with EAL 5, they are going for 7.

I’m not surprised, btw. Neither by their approach nor by their somewhat typical french building strong on math. The former looks reasonable; they seem to basically build along the line “Minix 3 but better and with a strong security focus” (which isa quite reasonable basis). As for the latter, oh well, Leroy and some others have created something serious there with one of the side effects being that they are a little playful with formal tools. Reminds me somewhat of the old days when a new system also got its own language. Now, with the french, every other project seems to get it own formal toolset *g
The french have managed to always keep the math skills of their students /at least at their better universities) sharp and if they now reap the benefits of that wisdom I can easily look over some waste and toying.

That kaspersky thingy is on a quite different (and dimensionally lower) level. Note, in particular that kaspersky seems to carefully avoid using the word “formal” when marketing-droiding about “verified”.

Btw, I personally couldn’t care less about EAL, Inegrity and whatnot. I want to see good engineering and proofs and the french, and to a degree the swiss and some others (funnily ones one wouldn’t think of) deliver (e.g. muen). Nice to see.
On a sidenote I’m bewildered how the germans, who had strong cards both with, for instance, L3 and L4 (or Alice) and with a rich and strong industry base could get so weak. Once the leaders they have fallen back nowadays.

On another sidenote I perceive the situation as the french going for know-how and real solutions while the germans seem to go for political and economic muscle (and hence for yet another fiasco (haha)). I found pikeos interesting but in no way leading. But with enough market muscle the germans might succeed to force-feed it as the “european security solution”.

ab praeceptis • November 20, 2016 11:44 AM

Nick P

1 to 4 can be widely interpreted. Why not “formally spec’d, modelled, proven”?
5, too. Why “shown” and not “proven”?
6, 7 is rarely really feasible. Funnily, I could live with that; it’s you (among others) who brings up, let’s say “not everyday”, situations like intentional EM use against a target.
8 is but lottery with good intention. Similar to the unit-testing religion.
10 is funny because experience shows that many weaknesses are created by admins or developers who just can’t be bothered to actually read, let alone follow good guidance.

Again: I agree with you that we should strive towards perfection. I partly disagree, though, re the means and in particular re the order of things. Before I try to make sure that seL4 is not just simply code verified (“perfection”) I strongly suggest to get rid of a couple of bazillion crap plastic boxes out there.

Noted my little hit on “unit-testing religion”? It nicely shows a point (and has something in common with fuzzy testing): I’ve seen loads of TDD evangelists preaching their religion. Then I took a closer look – and found the usual case to be “Formulate the requirement in terms of tests. Then implement till all test pass”. Done.

Sounds nice. And is BS. What do I really want to find in proper unit tests? Attacks, evil spirited cases, maximal insane user input. I do use unit tests and I use them for exactly that “evil” purpose; I use them against myself to see whether I really nailed it tight.

Let’s look at an innocent case: IP4 plus optional mask string conversion to integer plus integer mask.
Typical procedere: “that thing consists of 4 pieces, each up to 3 digits, separated by dots, plus optionally a slash followed by 1 or 2 digits” (rarely even a simple EBNF formal spec is done). Next step: build unit tests for “ip4str2ip4struct(char * ip4str, IP4STRUCT * res)”, i.e. throw some valid and some grossly invalid srings at it. Works? Done, great.
Comes a stupid user and enters the ip adress with commas. Fail. Oh and btw. there is no “const” with the ip4str and the unit test doesn’t care about that. Maybe it doesn’t care about “2000” (in an IP4) neither or about “351”. The mask var (I’m generous here) is declared as “char” (never mind a user entering “/33” …) and chances are that the ip var is declared “unsigned int” (rather than “uint_32”), etc, etc.

How do you “Clear[ly and] precise[ly]” nail that down? Write a book for that function? Forget it. There will be users coming up with idiocies you’re not even capable of dreaming in a nightmare. Plus hackers, of course who so the same but more or less knowledgeable-

There is just 1 way to properly nail that down: formal spec. Any eal or integrity or secbla asking for less is of little worth.

ab praeceptis • November 20, 2016 9:43 PM

Nick P

I’ll start at the end.

“Everything I cite came from real-world use” – yes, but there’s a difference between reading and citing and real world development.

Example: “hodgepodge lego”. You completely mistook that and immediately answered from a theoretical view. I, however, was talking about a case that pulled something you said (~ “I’d take this or that parser”) down to reality. Actually it’s touching an issue of great importance. You know what is probably the single most relevant criterion for language selection? -> availability of tons of libraries.

Now, assume (to pull something down to reality) you had to do your project in Pascal. But that damn super parser you mentioned happens to be written in ML. Sure, can be done, but is it efficient? Do you have the developers around who can do it? How will you make sure the binding isn’t spoiling something? Will the linker handle it? Can your static analyser deal with it? Etc, etc.

As for integrity, eal and similar (which you now for the second time just assert that I somehow failed to properly counter …). Let me put it to you in an ad absurdum/ad contrarium:

According to you we should then forget them cumbersome mathematical notations and proofs. Let’s instead use – I quote you – “Clear, precise description[s]”.

Do you finally see how untenable that line of argumentation is?

On top of that it’s practically useless. What am I supposed to do as a developer? Write the whole Do178 shebang in a comment prefixed to my function and then write another comment for each item on the list in my code?

What the hell does “this subprogram fully meets the specification” mean when the specification is “Clear, precise description”? Do you think more than one generation of compsci people have worked on formal methods and tools because they were bored?

Read Prof. B Meyer and others. There is but one “Clear, precise description” – and that is a formal one. And there is but one “Clear, precise and credible” assertion “routine ABC meets specification” and that is a formal one. Everything else is at best well intended words.

And as we just talk about it. Let’s say I have a formal spec in [insert favourite spec. method] and that I have, say, a pascal implementation – now what? That’s no fun question! That’s where we still have an itch. Unless my, say B tool can speak with my (non existing) Pascal analyser and vice versa there will again have to be a person – and a knowledgable one at that – to compare one to the other and to see whether implementation meets spec.

Let’s look at heartbleed. The problem there wasn’t simply a buffer overflow (that could be caught by a boundary check). The problem was the content of “unused array elements”. In other words: To check that no “Clear, precise description” will be of any use. You’ll need separation logic. Now, how many units, how many condition lines have you done in Verifast? Trust me, that’s not something you’d give to just the first developer around the corner nor to just some student.
Multiply the pain by cross checking that against the formal spec (which only very few methods will allow in the first place). Multiply that again by not having any analyser for Pascal, let alone one understanding sep. logic.

“Clear, precise description” is cheap – and but a lousy substitute for formal methods. But, to be fair, it was the best that was feasible for many years and to a degree still is (e.g. with Pascal).
And, quelle surprise, what are the eal & co more and more go toward? Formal methods.

Finally, you might want to extend your research to the practical realm. Let me tell you why: In a paper things look great. Did those guys ever produce more than a POC or a toy for them to test their ideas? Chances are: No. In case they did, is that tool still alive (let alone maintained)? Chances are: No. In case it is, does that tool run on a halfway current OS version and on an OS you happen to use and know? Chances are: No. In case it is, ist it also available for both x86 and amd64? Does it ask for reasonably modest lib dependencies, etc., i.e. is it practically usable with what you have and have to work with? Chances are: No.
Plus many, many other factors, some of which we occasionally mentioned, like: Is it java or .net only, or windows only, or in weird language without even a reasonable runtime lib, or does it ask for your sould to be sold (license), etc.

You’ll find out that very, very, very, few of those thingies in papers are actually of practical use in the real world.

And that IMO is one of the major reasons why we have so much crap out there. do178, eal? Changed next to nothing except for some “we don’t care about budget” (or “dman, it’s mandatory and they are serious about it”) niche projects.

I find it btw. disgusting how you belittle the work done with Larch for the Modula library as if it was but some weekend job by students. What those people did at that time was a warp leap and we wouldn’t have MANY problems if similar “toy afternoon” libraries were available.

ab praeceptis • November 21, 2016 8:55 AM

Nick P

Paper based theory, again.

For a start you are arguing with vague definitons and views. Example: OpenBSD.
Those guys are great, no doubt, they try seriously hard and they are experienced and good at it. But: That’s a very different goal post from the kind of security we talk about here.

To put it bluntly, OpenBSD’s goalpost could be described as “not creating crap” (Anyone who has read anything from me knows that I consider that very important and laudable).

But high safety? Forget it. So, fumbling with OpenBSD in this context here, and then in the next paragraph with, say, seL4 is rather, uhm, let’s call it inconsistent.

Btw, let me tell you a funny way to get quite decent code: Create it with Sather or, more modern, with Parasail or Leon.
In other words: One of the few things we should have solidly learned is that C is a very useful meta-assembler but not a PL per se. One can, of course, abuse it as a “high level” PL and that has been done a bazillion times – but we all know the crappy result.
Bernstein coding his chacha reference in C is one thing. Joe and John corp. developer coding an OS in C is a very different thing.

Back to the matter. We use formal notation to capture and convey meanings, qualities, quantities, etc. in a complete, unambiguous and precise manner. Human language, no matter how bent for a purpose can not provide that, at least not with any bearable efficiency. Simple as that. Plus: I as a non native speaker might easily mistake some do178 language but I will certainly not mistake a formal spec.

What it can provide, though, is understandability for humans.

Obvious Conclusion: formal spec plus human oriented annotations. ** not the other way around and f*cking certainly not without the formal part **.

I don’t care about all your papers and studies and “experience shows”. I have my own decades of experience and those are speaking a very clear language. Don’t get me wrong, I’m not hating C, quite the contrary; I’ve taught C, I’ve done uncountable loc in C and I would still urgently recommend it to any young developer – the same way I would recommend high-schools to teach Latin (and for very limited use).

C itself is not properly nailed down. Way too many ambiguities and things left to the implementors. Ergo: No matter how smart your wordy do178 or eal specs are, no matter how good your developers are, no matter how smart your spec to code generators are, there will always be some lottery left.

Microsoft is pimping up hundreds of thousands of loc with Hoare triples, proper boundary specs and other means. Certainly not for the fun of it. And it would seem to me that thay, having eal and do178 and whatnot golden stickers after all, certainly weren’t easy on “precise” blabla specs. Let me tell you the funny part: Doing that they found (to put it extremely diplomatically) many errors.

So, kindly stop telling me “experience” from papers and studies.

Or look at all them post factum analysers thrown at major code bases. Although these may not possibly perform properly as they have no formal “skeleton” to work along but rather must somehow try to make sense out of C code, they still found thousands upon thousands of bugs. Well noted, some of the software tested was eal, well word spec’d etc.

Now, look at Pascal code (not that I want to recommend Pascal for safe and secure but it’s well known, simple, about the same age as C, etc.). Way less problems. Reason? Less ambivalent, better nailed down and, let me call it “fragments of formal spec”. Sounds big but is true. Look at ranges. Those are some kind of (primitive – but very, very valuable) formal spec. Or look at “First” and “Last” loops; some kind of formal spec, too (a very primitive but powerful loop invariant).
And, as an important side note: Pascal simply doesn’t allow certain kinds of human errors thanks to that.

Finally, a do178, eal and whatnot spec’d C library may tell me – the human – a lot in its spec. But not my compiler. It may or may not do what it says it does and the way it says it does.
Proper pre- and postconditions, on the other hand, tell both me and the compiler a lot more. Granted, I give you that, those conditions may look gibberish to many and aren’t easy for the uninitiated, but they serve the job very well – and we all want core infrastructure devices safe, more than anything, right. Moreover the gibberish can be commented. Plus it depends in the tool. The Spark stuff, for instance, is rather human friendly. B (which I don’t use but like) is another sample and from the spec corner; quite friendly und not too hard to use.

ab praeceptis • November 23, 2016 7:18 AM

moz

“…voting machines, specifically those without paper records, may have been hacked or otherwise abused during the US election”

I just refuse to believe that. That’s so in-cre-di-ble!

I happen to know through diligent study of PR material from major voting machines manufacturers like “bend and adapt inc” and “desired results corp” as well as from the governments “super duper extreme totally awesomely fair elections” PR agency that the allegations you make are absolutely not possible.

In fact, I happen to kow that a poll was made using those very machines that clearly proves that 134% of the population are “perfectly happy and fully convinced” (trademark) with their voting machines working perfectly well and unbiased.

P.S. Kindly refrain from using the term “cyber-100%-trust” as I intend to trademark it and to earn lots of money with and to then buy my lovely auntie a governors post or a congress seat.

ab praeceptis • November 24, 2016 11:24 AM

r

Of course, the f*cked ones are the sailors.

And no, no “join’em mantra” whatsoever. I’m pissed over the edge how nonchanlantly the lamettas don’t give a sh*t about their sailors or, being at that, about OpSec.

Plus, unlike sailors they are protected; the victims will once more be the common man, in this case the sailors.

Finally, I think they should stop to make lots of noise about “evil Snowden” and begin to care about their job and their people.

ab praeceptis • November 24, 2016 2:33 PM

moz

I’m rather cold-blooded and tough on that whole election issue. Well noted, I’m not for either candidate; besides not being us-american anyway, if I would have a position at all, it’d be anti both of them.

Of course there was fraud! Probably even massive fraud.

We know that the dnc acted inacceptably, we know since at least 16 years that your elections are a scam, we know for many years that the machines of “desired results inc.” are biased, bent, and probably not even election machines but devices to remote generate the desired outcome while running a pure “elections” show like a computer game. People love clicking and people love the feeling that they have anything to decide …

Same story with your ridiculous “peoples vote” vs. electoral system.

Well noted, I have no position on that; do as ever you please. BUT: One doesn’t complain after the election show! If the us-americans had any real interest whatsoever, they had decades to take care of that.
It’s really simple. If I think, someone severed my cars brakes and I know that then it’s a wise thing to take care of that before driving every 4th year rather than complaining right after crashing.

Finally: What do they want? What do they expect? That “counting” again the fraudulent numbers of “desired result inc” machines will lead to another result? And I also find that whole thing funny because from clinton we know that they played games while from Trump we don’t; it’s just lots and lots of noise. Chances are that a “recount” would actually go against clinton. Then what? A re-re-count?

From what I as an outsider see that’s exactly the message by the people. They have damn enough of the large city crowds and the polit mafia (of both sides). From what I see the usually unheard (as in “ignored”) part of the population had enough and now the part that always makes lots of noises and demands safe spaces is doing what they always do: they’re making lots of noise.

That’s also why I see halderman so negative. Where has that “expert” been all those years? Why doesn’t he have tangible, credible, and actionable professionally processed data rather than making lots of “could” and “might” noise?

Yes, that whole election circus system is rotten. But it’s your system and I suggest that you use the next 3.5 years to repair your brakes which are known to be rotten before driving again on election road in 4 years.

Trump is your president. May he be a good one for you (and us).

ab praeceptis • November 24, 2016 4:42 PM

Thanks to certain contacts in the alaska secret service I happened to get my hands on the fec/eac election machine checksum verification code. Here it is:

#include <stdio.h>
#include <unistd.h>

int main(int argc, char **argv)
{
printf(“FEC/EAC official checksum checker. Tampering strictly forbidden!\n”);
printf(“V. 42. Selfverified. XR Code: ff42beef \n”);
if(argc < 2)
printf(“Checking all sensitive files.”);
else
printf(“Checking file ‘%s’.”, argv[1]);
printf(“Setting up verification engine …\n\n”);
sleep(1);
/* Show them we’re dead serious and very, very competent /
printf(“Cross verification (Mussorgsky-Schiller muon collision cross verification)\n”);
sleep(2);
printf(“Result: .\n\nChecksums match: 8d3c886d2c5a5a78a29e4ba86eae298e\n”);
/ Now, let’s finally play leisure larry */
return 0;
}

ab praeceptis • November 24, 2016 7:33 PM

How can you say such evil things?

They have adobe acrobat security!

What I find a little suspicious, though, is that there is neither mandatory AV nor 32-bit RSA.

ab praeceptis • November 25, 2016 5:36 AM

Ratio

I’m – positively – surprised. It seems there was a humourous undertone towards the end.

The problem though is that I don’t know of a good static verifier and spec tools for html. The one I currently use is this blogs comment section but it’s a little short on error messages, limiting itself to telling me “You html idiot!”

ab praeceptis • November 25, 2016 6:55 AM

Ratio

“Nick P is already at it”

And you? Where are you? It seems to me that Waels task for you and Nick P’s work would perfectly match. Object oriented DOS batch scripting is all but screaming to be used for that static analyser and formal spec tool for html.

Oh and: No exceptions, please. (In case I failed: This was an attempt at an insider pun: OO … exceptions)