GNAT Pro and GNAT Pro High Integrity Edition have certainly been used as the compilers for military systems.
GNAT, as the subject line suggests, is a GPL'd piece of software: the 'Pro' part relates to the level of support offered, access to prebuilt binaries for cross environments, early access to supported builds that are otherwise only visible in CVS GCC builds etc.
Those who are interested might look at Ada Core Technologies website.
Our company issues "Corporate" Amex cards to use for business expenses. Guess who American Express calls if the bill isn't paid?
Well, the answer to that question is 'it depends what kind of Corporate card you have'. Certainly, in the UK, American Express issue three different types of card, where the risk burden falls in different places.
I have a Corporate Card where (as I remember it) I am responsible paying for the charges incurred, but my employer and myself are jointly and severally liable for the balance. So if I don't pay, American Express can chase my employer. On the other hand, AmEx did carry out a credit check on me before issuing the card.
I believe there are two other options, with increasing levels of centralised billing and responsibility. I can't exactly remember the details, but I believe that one of these involved sole company liability.
Even if Palast and the Observer had "proof", truth is not an absolute defence under British law. This is why holocaust deniers are able to sue for libel when people call them "holocaust deniers". (The holocaust-denying plaintiff lost the lawsuit, but only because the judge ruled his "reputation had not been damaged"; not because of the truth of the defendant's statements.)
Justification - the defence to an action in the tort of defamation that the allegedly defamatory material is true - is an absolute defence.
I don't know where you got your information about the Irving case, but if you actually read the article to which you link, the ratio decidendi does not depend on the lack of damage to the plaintiff: the judge is quite clear that the truth of the accusation is the important fact.
By writing code in a language like SPARK (an Ada83 subset), you can then use mathematical tools to formally prove each part of your code to be "correct".
Just to point a few minor inaccuracies here: firstly, SPARK is not an Ada subset at all - although the executable part of a SPARK program is always a valid Ada program, simply writing an Ada program with the subset of executable statements that is defined to be SPARK will not result in a SPARK program.
This is because SPARK has non-executable annotations (which look to an Ada compiler like comments) which are used for static analysis of data and information flow, and also for proof.
Secondly, even if you do regard SPARK as an Ada 'subset', the recent versions should certainly be regarded as Ada 95 derivative, rather than Ada 83.
The reason why I put the word "correct" in quotes is because there is no good, formal definition of what "correct" means. The code may be provable to do exactly what you intend for it to do, but that's not necessarily the same as what it should be doing.
Good requirements capture and specification are obvious prerequisites to good software: the software engineering discipline does not begin where one starts to write code! The chain is clearly only as strong as its weakest link; historically, however, actual software implementation has resulted in bad, buggy and dangerous software with alarming regularity. Strong static analysis and proof tools can do a lot to minimise that risk when used properly.
So, hands up who has a soundcard with a digital-in. Keep your hand up if you have a CD audio player with a digital-out. Keep your hand up if you are a country music fan, and you make your own MP3s.
Well, let's assume there's one hand still raised; that's all that's needed for this particular CD to be ripped (in the digital domain) and placed onto [insert your P2P MP3 sharing system of choice here].
Well, that wasn't that hard, was it? Looks like the only people who are going to be truly inconvenienced by this are those want to exercise their (jurisdiction dependent) right to make a backup copy of their CD, and don't have the hardware or the technical know-how to circumvent this.
Is anyone seriously surprised that Q3A for Linux sales are low? If you have the Q3A for Windows CD, all you need to do is download the Linux binary and you are away...
Given that Q3A for Windows was released a significant period before the Linux boxed version, it seems probable that most of the gamers that wanted it already had it by the time the 'Linux specific' product was released, no?
For what it is worth, I own a Q3A retail pack - the Windows version thereof - that I have never played under Windows. Given that there's practically nowhere in the UK that you can buy Linux gaming software retail (there are a couple of mail order places), I don't find it at all surprising, personally. Games, for me at least, aren't things I want to mail order, wait for, pay shipping charges on, etc.
Maybe they should add a 'half sale' for each time the Linux Q3A binary package has been downloaded from their website...
Unlimited distribution is what we have. Why would we consider giving it up now? Communism, shmomunish. When resources are unlimited, price falls to zero. End of story.
Not end of story: Price falls to zero, cost/benefit ratio to original suppliers tends towards infinity, original suppliers all change business, economy collapses with a billion consumers, a hundred thousand distribution systems, and no new product.
How nice of you to imply that our Founding Fathers were Communists.
How nice of you to assume (despite a reasonable amount of evidence to the contrary) that I'm an American... Also, whilst you may have some belief that a group of jurists from the 18th century somehow foresaw the momentous developments in technology, and the implications thereof, I do not have that faith.
Your comments about control of information being the only way that value is generated do not hold up to scrutiny.
Incorrect. But don't feel bad; Lars made the same error in reasoning in a new interview in the San Francisco Examiner.
Digital artifacts are not being transferred away from one party toward another. They are being duplicated, such that both parties now have the artifact.
This attitude is, frankly, beginning to wear a bit thin.
The digerati-post-copyright, its-not-your-fault-you-don't-understand thing, that is. Excuse me whilst I generalise wildly from your position to encompass some of the things that annoy me most.
On the one hand, you're attempting to persuade people that digital distribution is the way forward, and that physical movement of information is destined to go the way of the dinosaurs (cf. Nicholas Negroponte et al.); that the net.economy holds information as its most valuable commodity, and has potentially unbridled potential - because the only natural resources required are ingenuity and graft (cf..com stock billionaires etc.), and the only barrier to entry is setting up your dialup connection.
At the same time, you're attempting to undermine the only, currently effective means of protection available to intellectual property - copyright. Napster exemplifies copyright violation writ large, nay, bloody huge.
Napster is, from an ethical standpoint, unsupportable. Most everyone who uses it thinks that they're doing wrong. Those who do seek to justify their positions do so in ways that would make most ethicists blush.
It is an interesting thing to consider that -- given the hypothetical of a corporation conducting a business that profits from an immoral traffic, and attempts to defend itself by deliberate inadvertance -- I feel many/.'ers would cry 'foul', until the N-word contextualises it.
All the time that Napster stays in business in its current form, the notion of intellectual property becomes eroded. We are creating a generation who believe they have an entitlement to take... excuse me duplicate whatever they want, and [cannot|do not wish to] pay for, within the digital domain.
The RIAA itself may represent a cartel of sorts, and may have some morally reprehensible aspects of its own, but - proverbially - two wrongs do not make a right.
Napster is a parasitic response to a problem; the problem is, of course, technology advancing at too fast a rate for economic models to keep up. There is no reasonable framework in place to support micropayments, oft-touted as the 'magic bullet' to cure the problem. There is no reasonable method for artists themselves to exercise control over their work, nor technology available to enforce that.
Napster is the technological chimera that is filling the gap between the advent of the possibility and the maturity of the model; it leverages the technology irresponsibly, feeding off the human desire to have for free what one should have paid for, and the negative public opinion towards the major labels. It gives back nothing to the artists, and in doing so it lines its pockets.
In the real world, Alice wouldn't mind too much if Bob fed her BMW into a 'car copier', and got one for himself. As you say, no-one _really_ loses (assuming Bob would otherwise have been able to afford the car).
Unfortunately, if you're going to be consistent with your rhetoric (God forbid), you're going to realise that the same does not apply in the digital economy. The only way that value exists in such an economy is through control of information: it is in the gradients of information flow that value is added... I might pay to know what you know, or to hear your music, or whatever.
The concept of unlimited duplication is absolute anathema to this concept. The idea that everything should be redistributable without limit, in some kind of pseudo-Utopian way, is actually the digital equivalent of forcible redistribution of assets - Communism for the Net Age, anyone?
How to deal with these issues is a hard question. I don't have the answers (although I have some bits and pieces). What I do know is that Napster is not the way forward. A concept of intellectual property is vital to a realistic, future digital economy. Napster undermines this from one day to the next, and in doing so it threatens to sabotage the potential of that economy.
Then some 5kr1p7 k1dd13 stumbles on an exploit and suddenly the bulk of the world's computer users is vulnerable.
I think you're rather overestimating the typical level of skill and competence possessed by the average script kiddie.
Most anecdotal evidence (and certainly my server logs) point to the fact that most attacks consist of running whatever tools they have over whatever hosts they 'like the look of'. If nothing cracks, they move on.
I don't honestly think that, if the tools were to dry up, these same kiddies would actually bother to learn about the theory and practice of security. I'd bet that most of them don't even understand how TCP/IP works, or know how to program beyond a trivial level in C.
There is an annoying elitism among functional programming proponents, implying that all current Perl and Python and C++ programmers are wrong.
I think that's strong - I prefer Philip Wadler's construction of this idea (from an ACM SIGPLAN Notices) under the title of non-reasons for the lack of general adoption of functional languages:
"They don't get it" Functional programming is beautiful, a joy to behold. Once someone understands functional programming, he or she will switch to it immediately. The masses that stick with outmoded imperative and object-oriented languages do so out of blind prejudice. They just don't get it.
He holds this up as a mistaken belief frequently held by researchers. I don't think its arrogance, I rather think it's the kind of thing demonstrated by excessively evangelical, newly converted Christians who want everyone else to 'see the light'.
Some FP proponents insist that functional laziness is the key. Others think that laziness is unpredictable and does more harm than good. [etc]
Well, this is still very much a research field. Issues like mutable state in functional languages, controlling dragging caused by excessive, uncontrolled laziness, etc. are hard - and I think it's a good thing that people are trying different approaches.
To be fair, most of the debate centres around purely functional languages, which are of significant research interest: you can quite happily write industrial strength, concurrent distributed systems with functional languages - cf. the Foxnet server discussed elsewhere on this thread, and the use of Erlang by Ericsson for the software for some of their ATM switches.
Many FP language developers would prefer to do research on new type systems, rather than create useful libraries. Many think that language choice is more important than tool choice, as if ML would somehow be better at GUI-driven applications than Delphi.
Most FP language developers are not software developers, stricto sensu: they are computer science researchers! It is 'what they do', to do research on things like type systems. It seems a little unfair to criticise them for this. I have honestly never seen the 'language choice more important than tool choice' attitude in the functional programming community: people may have strong views (academically) about whether strict or lazy semantics are to be preferred, but they are not so blindly partisan as you paint them.
In sum, the fact is that functional programming is (in most cases) on the cutting edge of programming language research; as such, there are bound to be academic debates about the merit of one approach or another.
I don't think static typing is very mathematical anyway.
You're kidding, right? Have you ever looked at the way a Hindley-Milner type inferencing system works? And noticed that the inference rules correspond almost directly to the rules of intuitionistic logic?
Everyone who's used ML can attest to this fact: once your programs typecheck, they Just Work.
This is a myth. I agree that it does prevent certain types of errors, but not others. For example, suppose you have a function that draws a rectangle: rect(x,y,width,height). You forget and pass the parameters like this instead(x,width,y,height). The type system won't catch the error, because all the values are integers.
Yes, but that's bad design. You could have different types for co-ordinates, and for lengths. My experience with Haskell and ML has overwhelmingly led me to believe that strict type systems are a good thing.
I hear about multiuser systems being banned for security reasons and it really bothers me. Getting root is not significantly diffrent from getting admin other than one is on Unix and one is on Windows.
I'd disagree here; you get Administrator access on an NT box remotely, and what can you do? Not very much, if we're honest.
Get root on a UNIX box, and you've got a shell that lets you interact with the machine, run arbitrary programs etc.
One of the weaknesses of NT; namely, it's inability to be managed remotely 'out of the box', is an advantage when it comes to getting attacked remotely.
Internet cafes see a lot of people using telnet to access university accounts during holidays. Until the ubiquitous Windows-based net cafes around the world all get ssh, this is going to piss some people off.
For what it's worth, the PuTTY SSH client for Windows is only a few hundred K, and is a monolithic executable; it doesn't have any configuration files floating around etc.
If running your own executables is disallowed, then you have to look to other options: most cyber cafes allow Java, right? In that case, you probably want to look at MindTerm - a free (GPL'd) Java SSH implementation.
Besides which, university accounts ought to have decent security to protect root. So there are a few dodgy logins here and there. It's worth it just to be able to read your email anywhere.
I don't think there's any excuse for poor security, when it only takes a few minutes of web searching to turn up good alternatives. Also, it's not just 'a few dodgy logins' - compromised accounts get an attacker through the 'security perimeter' of the network, an easy way to get past external firewalls for example. They also provide an excellent staging post for attacks against other systems on the network.
Given that SSH implementations are now available on most any platform you care to mention, telnet should rightly be regarded as a legacy protocol. Anonymous ftp obviously has its place, but the 'nonymous' version could easily be supplanted by SCP style functionality
kawaii wrote:
Except that on Windows, ssh is not a stock part of the OS (there are/no/ free versions that I'm aware of, and even the pay versions don't seem to support tunnelling[1], etc), and there is no secure way to access email, ftp, etc. IMHO this is one of the worst aspects of Windows (low emphasis on security), but it means that there is no way to force security without more work than most people are interested in.
You need some PuTTY - it makes Windows usable. It's a free SSH client for Windows, that also (if I remember correctly) supports port-forwarding etc. It is released under the MIT licence (kinda similar to the BSD licence) which is 'Open Source certified'.
Just as an aside; how recently is it that SSH has become a standard part of Linux distributions?
I used to work as the network manager for a college, which had a couple of hundred ethernet sockets in student accommodation. Here's my take on this and on why I think it's likely to be less of a problem in the future.
Why are unencrypted protocols so much of a problem?
The main reason why telnet (particularly) is singled out as a security culprit is that's so trivial to harvest passwords, if you have the potential to eavesdrop on a network connection. The username and password are transmitted in the clear, right at the start of the connection: all you need to do is grab the first hundred bytes of any connection to port 23, and you'll get 9 out of 10 passwords.
Why is eavesdropping more of a problem in the residential network environment?
The residential network environment is chaotic, and there is usually very little capacity for control of what is physically connected to the network. I've heard of administrators who are getting serious problems with their ethernets, who eventually track the problem down to a student with a hub in their room, or whatever.
Ethernet is (in its basic form) a shared-media broadcast protocol; everyone gets everyone elses packets as well as theirs. Zap your adapter into promuiscuous mode and there it all is. There are two basic ways around this from the hardware perspective. You either go for switched ethernet (which was traditionally been prohibitively expensive for the relatively low priority residential networks), or need-to-know hubs, which track the MAC addresses attached to each port, and scramble the data that goes to the others (for example, the 3Com SuperStack II portswitch hubs); both of these technologies have been significantly more expensive than the sort of baseline kit that has traditionally been specified in campus LANs.
Aggravating risk factors
We're seeing a lot more students running multiuser systems; Linux, *BSD, whatever. These are quite often not the best maintained machines. They are relatively frequently subjected to root exploit, and are less likely to be quickly detected as such than well run systems.
Also, the prevalence and reliance on network services is on the increase. As the density of usage increases, so increases the potential for catastrophic breaches of security. It is not unheard of for thousands of accounts to compromised by a sniffer attack from a rooted Linux box.
Why the future is rosier...
For a start, networking kit that isn't susceptible to sniffing attacks is becoming cheaper. I personally got budgetary approval to replace all our hubs with need-to-know hubs, and my successor is installing switches to service student ethernet ports.
IPv6 is on its way; hopefully bringing network layer encryption and authentication. This is the ideal solution; SSH is great, but this sort of stuff should not be going on at application layer.
There is a significantly greater awareness of the issues on the part of university technical staff. I reckon some of the security people here know more about 'r00t-kits' and 'skripts' than most of the 'kyddies'. This also trickles down into the administration: they realise its bad press to be hacked, and it's also tremendously expensive to recover from it. Coupled with the decreasing costs of doing it right, as mentioned above, it means that 'network security' is becoming a higher budgetary priority.
In summary...
The campus networks that are being installed today are probably highly resilient to being snooped, but there are a lot of legacy installations, based on equipment that's possibly 3-5 years old, that is horrifyingly insecure. Ideally, in the future, we won't have to worry about layer-2 insecurity, because we'll be protected by the IP network itself; however, in the meantime, SSH Is Your Friend!
Idon't mean to get alarmist, but the biggest thing that scares me about this is the fact that it wasn't a workplace, or a repressed nation, or a government agency that was approached with these "solutions" - it was schools. Campuses. Institutes of higher learning, where people go to get an education. You know, where the frontline of defense of our rights has always been held, by protest or otherwise.
Sorry, but did you even read the article? The presentation that is alluded to in the story places a strong emphasis on the rights of individuals; especially on the privacy perspective.
The point seemed, to me at least, that telnet and ftp were (for campus networks) very insecure protocols. Anyone who's ever run a packet sniffer on a shared media ethernet can testify to this. Yes, ideally all the college residential networks would be switched, or protected by Need-To-Know scrambling hubs (cf. 3Com SuperStack II PS). However, this equipment tends to be more expensive than 'dumb' hubs, and wiring of accommodation does tend to be a lower priority from the funding perspective.
We're now seeing students running Linux boxes from their dorm rooms, connected to such shared networks. We'll assume that their honesty isn't in question (however spurious such an assumption may be!); the fact still remains that such boxes are frequently ill-maintained and the subject of frequent root exploits. Once you've rooted a machine on a shared media network that runs a lot of telnet/pop/ftp, it's trivial to harvest large numbers of passwords: and don't say it doesn't happen, because I know for a fact that it does.
Given that SSH implementations are now available on most any platform you care to mention, telnet should rightly be regarded as a legacy protocol. Anonymous ftp obviously has its place, but the 'nonymous' version could easily be supplanted by SCP style functionality.
Besides, aside from physically SHUTTING DOWN the entire internet (an impossible feat if there ever was one by now) how can they protect us from ourselves, as they seem to feel they need to?
I don't get the impression that what's being talked about is 'protecting' the tech-savvie user from themselves; but rather protecting the typical user from their ignorance. There isn't a good reason to retain telnet for passworded account logins; spewing off about shutting down such services effectively being the thin end of a wedge that ends with 'SHUTTING DOWN' the internet; well, that just looks silly.
I agree wholeheartedly with the presenter's point: I'd go one step further - it's not just telnet and ftp that present the problem; IMAP and POP are also generally insecure, not to speak of the numerous HTTP-based webmail services. The solution here is less clear-cut: nice alternatives like SSH are not widely available. Roll on IPv6 and network-level encryption, eh?
Nice post, but I'm not sure what you mean when you say the `open source development model does directly contradict most of the software enginerring principles that are called upon in the development of trusted systems'. Do you have a specific contradiction in mind, or are you just making a an assertion about hacking culture?
I think there are specific contradictions, as well as a more general cultural problem.
From the viewpoint of specific contradictions: there is, in the trusted systems world, a certain emphasis on the importance of specification. Now, to my mind, the concept of a formal specification, and of development guided entirely by a codified specification, sits all at ease with the open source development model.
As stated elsewhere, it is the evolutionary advantages of open source development that seem to be their keenest asset; but one important thing when it comes to trusted software is getting it right, first time.
When it comes to getting it right, from a trusted systems point of view, there is also the requirement to prove you have it right. Now, I've never seen an open source project developed using anything approaching formal methods; I would be interested to be corrected on this, though!
To be still more specific, and to focus on TCSEC as a source of authority on what constitutes trusted systems 'best practice', the open source model is almost the antithesis of desirable life-cycle assurance: Orange Book calls for steps to be taken:
to ensure that the system is designed, developed, and maintained using formalized and rigorous controls and standards
This connotes everything I mentioned above, and also implies extremely high standards of configuration management and regression testing. Similarly, there is a tremendous emphasis on documentation, which I feel is a weak point for many open source projects. The level of required documentation for high assurance levels is impressive: not limited to end user documentation, but also security policy and design.
The potential incompatibility between the highest assurance levels and the open-source model is evident from Section 4.2 of the Red Book - Beyond Class (A1); here, one specific area mentioned is:
Trusted Design Environment
The TCB must be designed in a trusted facility with only trusted (cleared) personnel.
I probably needn't say much more about this.
I notice that in that brief survey, I said rather more about culture than I intended, so I'll not make any other points about that; other than to say that I also feel that many 'hackers' just plain aren't interested in doing the boring bits required for trusted systems. Despite the fact that having a DoD/NSA approved system, no-one in the open-source world has done it yet.
PS. I note your email address is in Oxford: are you a member of Roscoe's group?
No; I'm currently working on my Masters thesis, which is concerned with functional programming; I'm supervised by Richard Bird. I notice that you were an assistant lecturer at New College... you probably know some of my friends!
"Trusted Software" or trusted systems in general are supposed to meet a spcification that was written by the DoD in 1983 (which was an update to docs written in the early 1970's) that outlines appropriate guidelines for access to remote systems and embedded software.
That's almost correct: at this point, you're referring to Orange Book, or DOD 5200.28-STD. It was last updated (as far as I know) in 1985. Otherwise, I agree.
However, remote access to systems is a job not only for the operating system of the host, but also for the network it runs on. Being that networks in 1983 were a little different than they are now, I would hope that a system that was meant to provide access to possibly classified data would rely on more than simply the security of the selected operating system, regardless of the openness of the sourcecode.
Orange Book is specifically about computer systems, not networks, or indeed networked computer systems. If you're interested in what the NSA/DoD has to say about networked systems, then you should probably be looking at the Red Book; aka NCSC-TG-005, which is available somewhere on the NCSC's public webserver: Radium. This server is a tremendous resource to those interested in trusted computer systems; the nice people at Fort Meade will even send you a CD containing the full website, free of charge, if you ask them nicely.
When you get to high levels of trust, you cease to regard testing as an adequate assurance. You want to see evidence that the system has been specified carefully and correctly, and that the code meets the specification. Needless to say, if you don't have a specification, you can't be trusted.
pallex wrote:
Yes, but this just tests that what has been specified has been coded correctly. If people are just adding bits here and there, as in an open source project, such as Linux, then nothing is specified as such, but you can test the various bits just as well. Its just outside this particular development paradigm.
If the specification correctly embodies the requirements (enter, stage left, the requirements engineers), then what you've actually proved is that the system Does The Right Thing.
I'm not sure what you're getting at when you say 'you can test the various bits just as well', if you don't have a specification. What are you going to test them against? Your personal expectations? What if another developer has subtly different expectations?
What I'm getting at, basically, is that you can't prove shit about squat unless you have some kind of specification. And unless your specification has been done in a moderately rigorous manner, then even what proofs you can do are mostly worthless.
This isn't meant as a knock to the Open Source development model, it's just a harsh fact of life. Where proof is important, specification is vital, and historically that has tended to imply Cathedral, rather than Bazaar. I would be interested to see a large open source project done with a degree of formalism. In fact, if anyone is interested in doing something that way, I'd be interested to be involved!
Just because something is closed source, that doesn't mean it's developed to a formal specification with formalized testing.
Absolutely true; the overwhelmingly vast majority of software (be it open or closed source) is not developed to a formal specification with formalized testing.
That said, there are pieces of closed source software which do meet these standards, and are certified to do so; examples of these include the products that the NSA (via the NCSC) certifies as part of its INFOSEC programme. The development of such pieces of software (Trusted Oracle, whatever) is reviewed, the source code is inspected, proofs are drawn up that the security policies that are alleged to be maintained are in fact maintained. In some cases, one even goes so far as to verify the object code generated.
Furthermore, what constitutes a formal specification? Both OpenBSD and Linux derive their security models from the Unix security model. That model *is* a specification. But is it a *formal* specification, and if not exactly what constitutes a formal specification?
No; the UNIX security model does not constitute a formal specification. However, one could quite easily write a formal specification for the UNIX filesystem security model; in fact, it would be quite a simple specification. Formal specifications are usually written using a mathematical specification notation, accompanied by English explanatory notes. Such specifications have the advantage that they are unambiguous, which is a tremendous advantage over English.
However, even if the UNIX security model were to be formally specified, it is an insufficient model to be trusted to any real level. It is insufficiently fine grained at one level, and it is insufficiently strict at another.
TCSEC C2 and above require the implementation of DAC - Discretionary Access Control - which requires a finer level of distinction between users' access priveleges than is really possible with the simple capability bits of the UNIX filesystem, in its original form.
TCSEC B1 and above require the implementation of MAC - Mandatory Access Control - this is all about making sure that 'security levels' on data are respected: i.e. if Joe has Confidential clearance, and I have Secret, I cannot write my Secret data into a file that Joe can read; even if the DAC system would allow me. Similarly, Joe cannot read my Secret files, even if the ACL permissions I have set would allow it.
And that's only half the story: once you have a formal specification of your system security policy, you have to prove that it is invariant. That's tricky stuff, unless you're working from a specification in which it's inherent.
Also, "formal spec" is a loose term. To me, the phrase "Any user can use only services they are explicitly authorized to use" is a formal spec.
Formal specification may be a loose term to you, but it is not nearly so loose to (say) the Department of Defense.
For example, for the higher levels of assurance under Orange Book (DoD TCSEC), like B2-A1, a formal specification is required that allows proof that a system does not violate its axioms. Now, your specification may baldly restate this requirement, but it does not come close to discharging a proof obligation.
For A1-level assurance, the top level specification is required to be highly formal, including the requirement for a mathematical proof of the system, and also a proof that the security policy itself is sufficient.
Least of all the ISO 9000 stuff. ISO 9000 is the least formal doc I've read in a LONG time. It's worse than useless.
ISO 9000 is a quality certification that is about process, not about the standards required of a particular project. There are, however, objective standards (which do have those letter/number names you dislike so much!) which are relevant: things like DEFSTD 00-55/56, ITSEC/TCSEC, DO-178B etc.
It seems that there is a feeling that having a formal specification is simply a hoop that some people have to jump through before getting down to hacking. This is an unfortunate attitude, and (I feel) tends to undo the whole point of making the specification in the first place.
Slashdot Mirror
My Sony VAIO PCG-U1 has a 6.4" diagonal LCD, with a 1024x768 resolution - that has got to be about 200dpi or thereabouts.
It is impressively fine. I can't really imagine what a 22" version of this would look like.
... from the film WarGames
GNAT Pro and GNAT Pro High Integrity Edition have certainly been used as the compilers for military systems.
GNAT, as the subject line suggests, is a GPL'd piece of software: the 'Pro' part relates to the level of support offered, access to prebuilt binaries for cross environments, early access to supported builds that are otherwise only visible in CVS GCC builds etc. Those who are interested might look at Ada Core Technologies website.
Our company issues "Corporate" Amex cards to use for business expenses. Guess who American Express calls if the bill isn't paid?
Well, the answer to that question is 'it depends what kind of Corporate card you have'. Certainly, in the UK, American Express issue three different types of card, where the risk burden falls in different places.
I have a Corporate Card where (as I remember it) I am responsible paying for the charges incurred, but my employer and myself are jointly and severally liable for the balance. So if I don't pay, American Express can chase my employer. On the other hand, AmEx did carry out a credit check on me before issuing the card.
I believe there are two other options, with increasing levels of centralised billing and responsibility. I can't exactly remember the details, but I believe that one of these involved sole company liability.
For what it's worth.
Even if Palast and the Observer had "proof", truth is not an absolute defence under British law. This is why holocaust deniers are able to sue for libel when people call them "holocaust deniers". (The holocaust-denying plaintiff lost the lawsuit, but only because the judge ruled his "reputation had not been damaged"; not because of the truth of the defendant's statements.)
Justification - the defence to an action in the tort of defamation that the allegedly defamatory material is true - is an absolute defence.
I don't know where you got your information about the Irving case, but if you actually read the article to which you link, the ratio decidendi does not depend on the lack of damage to the plaintiff: the judge is quite clear that the truth of the accusation is the important fact.
By writing code in a language like SPARK (an Ada83 subset), you can then use mathematical tools to formally prove each part of your code to be "correct".
Just to point a few minor inaccuracies here: firstly, SPARK is not an Ada subset at all - although the executable part of a SPARK program is always a valid Ada program, simply writing an Ada program with the subset of executable statements that is defined to be SPARK will not result in a SPARK program.
This is because SPARK has non-executable annotations (which look to an Ada compiler like comments) which are used for static analysis of data and information flow, and also for proof.
Secondly, even if you do regard SPARK as an Ada 'subset', the recent versions should certainly be regarded as Ada 95 derivative, rather than Ada 83.
The reason why I put the word "correct" in quotes is because there is no good, formal definition of what "correct" means. The code may be provable to do exactly what you intend for it to do, but that's not necessarily the same as what it should be doing.
Good requirements capture and specification are obvious prerequisites to good software: the software engineering discipline does not begin where one starts to write code! The chain is clearly only as strong as its weakest link; historically, however, actual software implementation has resulted in bad, buggy and dangerous software with alarming regularity. Strong static analysis and proof tools can do a lot to minimise that risk when used properly.
So, hands up who has a soundcard with a digital-in. Keep your hand up if you have a CD audio player with a digital-out. Keep your hand up if you are a country music fan, and you make your own MP3s.
Well, let's assume there's one hand still raised; that's all that's needed for this particular CD to be ripped (in the digital domain) and placed onto [insert your P2P MP3 sharing system of choice here].
Well, that wasn't that hard, was it? Looks like the only people who are going to be truly inconvenienced by this are those want to exercise their (jurisdiction dependent) right to make a backup copy of their CD, and don't have the hardware or the technical know-how to circumvent this.
Is anyone seriously surprised that Q3A for Linux sales are low? If you have the Q3A for Windows CD, all you need to do is download the Linux binary and you are away...
Given that Q3A for Windows was released a significant period before the Linux boxed version, it seems probable that most of the gamers that wanted it already had it by the time the 'Linux specific' product was released, no?
For what it is worth, I own a Q3A retail pack - the Windows version thereof - that I have never played under Windows. Given that there's practically nowhere in the UK that you can buy Linux gaming software retail (there are a couple of mail order places), I don't find it at all surprising, personally. Games, for me at least, aren't things I want to mail order, wait for, pay shipping charges on, etc.
Maybe they should add a 'half sale' for each time the Linux Q3A binary package has been downloaded from their website...
Cheers, Nick.
Unlimited distribution is what we have. Why would we consider giving it up now? Communism, shmomunish. When resources are unlimited, price falls to zero. End of story.
Not end of story: Price falls to zero, cost/benefit ratio to original suppliers tends towards infinity, original suppliers all change business, economy collapses with a billion consumers, a hundred thousand distribution systems, and no new product.
Cheers, Nick.
How nice of you to imply that our Founding Fathers were Communists.
How nice of you to assume (despite a reasonable amount of evidence to the contrary) that I'm an American... Also, whilst you may have some belief that a group of jurists from the 18th century somehow foresaw the momentous developments in technology, and the implications thereof, I do not have that faith.
Your comments about control of information being the only way that value is generated do not hold up to scrutiny.
Then give an alternative.
Cheers, Nick.
Incorrect. But don't feel bad; Lars made the same error in reasoning in a new interview in the San Francisco Examiner.
Digital artifacts are not being transferred away from one party toward another. They are being duplicated, such that both parties now have the artifact.
This attitude is, frankly, beginning to wear a bit thin.
The digerati-post-copyright, its-not-your-fault-you-don't-understand thing, that is. Excuse me whilst I generalise wildly from your position to encompass some of the things that annoy me most.
On the one hand, you're attempting to persuade people that digital distribution is the way forward, and that physical movement of information is destined to go the way of the dinosaurs (cf. Nicholas Negroponte et al.); that the net.economy holds information as its most valuable commodity, and has potentially unbridled potential - because the only natural resources required are ingenuity and graft (cf. .com stock billionaires etc.), and the only barrier to entry is setting up your dialup connection.
At the same time, you're attempting to undermine the only, currently effective means of protection available to intellectual property - copyright. Napster exemplifies copyright violation writ large, nay, bloody huge.
Napster is, from an ethical standpoint, unsupportable. Most everyone who uses it thinks that they're doing wrong. Those who do seek to justify their positions do so in ways that would make most ethicists blush.
It is an interesting thing to consider that -- given the hypothetical of a corporation conducting a business that profits from an immoral traffic, and attempts to defend itself by deliberate inadvertance -- I feel many /.'ers would cry 'foul', until the N-word contextualises it.
All the time that Napster stays in business in its current form, the notion of intellectual property becomes eroded. We are creating a generation who believe they have an entitlement to take ... excuse me duplicate whatever they want, and [cannot|do not wish to] pay for, within the digital domain.
The RIAA itself may represent a cartel of sorts, and may have some morally reprehensible aspects of its own, but - proverbially - two wrongs do not make a right.
Napster is a parasitic response to a problem; the problem is, of course, technology advancing at too fast a rate for economic models to keep up. There is no reasonable framework in place to support micropayments, oft-touted as the 'magic bullet' to cure the problem. There is no reasonable method for artists themselves to exercise control over their work, nor technology available to enforce that.
Napster is the technological chimera that is filling the gap between the advent of the possibility and the maturity of the model; it leverages the technology irresponsibly, feeding off the human desire to have for free what one should have paid for, and the negative public opinion towards the major labels. It gives back nothing to the artists, and in doing so it lines its pockets.
In the real world, Alice wouldn't mind too much if Bob fed her BMW into a 'car copier', and got one for himself. As you say, no-one _really_ loses (assuming Bob would otherwise have been able to afford the car).
Unfortunately, if you're going to be consistent with your rhetoric (God forbid), you're going to realise that the same does not apply in the digital economy. The only way that value exists in such an economy is through control of information: it is in the gradients of information flow that value is added ... I might pay to know what you know, or to hear your music, or whatever.
The concept of unlimited duplication is absolute anathema to this concept. The idea that everything should be redistributable without limit, in some kind of pseudo-Utopian way, is actually the digital equivalent of forcible redistribution of assets - Communism for the Net Age, anyone?
How to deal with these issues is a hard question. I don't have the answers (although I have some bits and pieces). What I do know is that Napster is not the way forward. A concept of intellectual property is vital to a realistic, future digital economy. Napster undermines this from one day to the next, and in doing so it threatens to sabotage the potential of that economy.
(Flame: -1, anybody?)
Cheers, Nick.
Then some 5kr1p7 k1dd13 stumbles on an exploit and suddenly the bulk of the world's computer users is vulnerable.
I think you're rather overestimating the typical level of skill and competence possessed by the average script kiddie.
Most anecdotal evidence (and certainly my server logs) point to the fact that most attacks consist of running whatever tools they have over whatever hosts they 'like the look of'. If nothing cracks, they move on.
I don't honestly think that, if the tools were to dry up, these same kiddies would actually bother to learn about the theory and practice of security. I'd bet that most of them don't even understand how TCP/IP works, or know how to program beyond a trivial level in C.
Cheers, Nick.
There is an annoying elitism among functional programming proponents, implying that all current Perl and Python and C++ programmers are wrong.
I think that's strong - I prefer Philip Wadler's construction of this idea (from an ACM SIGPLAN Notices) under the title of non-reasons for the lack of general adoption of functional languages:
He holds this up as a mistaken belief frequently held by researchers. I don't think its arrogance, I rather think it's the kind of thing demonstrated by excessively evangelical, newly converted Christians who want everyone else to 'see the light'.
Some FP proponents insist that functional laziness is the key. Others think that laziness is unpredictable and does more harm than good. [etc]
Well, this is still very much a research field. Issues like mutable state in functional languages, controlling dragging caused by excessive, uncontrolled laziness, etc. are hard - and I think it's a good thing that people are trying different approaches.
To be fair, most of the debate centres around purely functional languages, which are of significant research interest: you can quite happily write industrial strength, concurrent distributed systems with functional languages - cf. the Foxnet server discussed elsewhere on this thread, and the use of Erlang by Ericsson for the software for some of their ATM switches.
Many FP language developers would prefer to do research on new type systems, rather than create useful libraries. Many think that language choice is more important than tool choice, as if ML would somehow be better at GUI-driven applications than Delphi.
Most FP language developers are not software developers, stricto sensu: they are computer science researchers! It is 'what they do', to do research on things like type systems. It seems a little unfair to criticise them for this. I have honestly never seen the 'language choice more important than tool choice' attitude in the functional programming community: people may have strong views (academically) about whether strict or lazy semantics are to be preferred, but they are not so blindly partisan as you paint them.
In sum, the fact is that functional programming is (in most cases) on the cutting edge of programming language research; as such, there are bound to be academic debates about the merit of one approach or another.
Cheers, Nick.
I don't think static typing is very mathematical anyway.
You're kidding, right? Have you ever looked at the way a Hindley-Milner type inferencing system works? And noticed that the inference rules correspond almost directly to the rules of intuitionistic logic?
It's certainly a mathematical task.
Cheers, Nick.
Everyone who's used ML can attest to this fact: once your programs typecheck, they Just Work.
This is a myth. I agree that it does prevent certain types of errors, but not others. For example, suppose you have a function that draws a rectangle: rect(x,y,width,height). You forget and pass the parameters like this instead(x,width,y,height). The type system won't catch the error, because all the values are integers.
Yes, but that's bad design. You could have different types for co-ordinates, and for lengths. My experience with Haskell and ML has overwhelmingly led me to believe that strict type systems are a good thing.
Cheers, Nick.
I hear about multiuser systems being banned for security reasons and it really bothers me. Getting root is not significantly diffrent from getting admin other than one is on Unix and one is on Windows.
I'd disagree here; you get Administrator access on an NT box remotely, and what can you do? Not very much, if we're honest.
Get root on a UNIX box, and you've got a shell that lets you interact with the machine, run arbitrary programs etc.
One of the weaknesses of NT; namely, it's inability to be managed remotely 'out of the box', is an advantage when it comes to getting attacked remotely.
Cheers, Nick.
Internet cafes see a lot of people using telnet to access university accounts during holidays. Until the ubiquitous Windows-based net cafes around the world all get ssh, this is going to piss some people off.
For what it's worth, the PuTTY SSH client for Windows is only a few hundred K, and is a monolithic executable; it doesn't have any configuration files floating around etc.
If running your own executables is disallowed, then you have to look to other options: most cyber cafes allow Java, right? In that case, you probably want to look at MindTerm - a free (GPL'd) Java SSH implementation.
Besides which, university accounts ought to have decent security to protect root. So there are a few dodgy logins here and there. It's worth it just to be able to read your email anywhere.
I don't think there's any excuse for poor security, when it only takes a few minutes of web searching to turn up good alternatives. Also, it's not just 'a few dodgy logins' - compromised accounts get an attacker through the 'security perimeter' of the network, an easy way to get past external firewalls for example. They also provide an excellent staging post for attacks against other systems on the network.
Cheers, Nick.
I wrote:
Given that SSH implementations are now available on most any platform you care to mention, telnet should rightly be regarded as a legacy protocol. Anonymous ftp obviously has its place, but the 'nonymous' version could easily be supplanted by SCP style functionality
kawaii wrote:
Except that on Windows, ssh is not a stock part of the OS (there are /no/ free versions that I'm aware of, and even the pay versions don't seem to support tunnelling[1], etc), and there is no secure way to access email, ftp, etc. IMHO this is one of the worst aspects of Windows (low emphasis on security), but it means that there is no way to force security without more work than most people are interested in.
You need some PuTTY - it makes Windows usable. It's a free SSH client for Windows, that also (if I remember correctly) supports port-forwarding etc. It is released under the MIT licence (kinda similar to the BSD licence) which is 'Open Source certified'.
Just as an aside; how recently is it that SSH has become a standard part of Linux distributions?
Cheers, Nick.
I used to work as the network manager for a college, which had a couple of hundred ethernet sockets in student accommodation. Here's my take on this and on why I think it's likely to be less of a problem in the future.
Why are unencrypted protocols so much of a problem?
The main reason why telnet (particularly) is singled out as a security culprit is that's so trivial to harvest passwords, if you have the potential to eavesdrop on a network connection. The username and password are transmitted in the clear, right at the start of the connection: all you need to do is grab the first hundred bytes of any connection to port 23, and you'll get 9 out of 10 passwords.
Why is eavesdropping more of a problem in the residential network environment?
The residential network environment is chaotic, and there is usually very little capacity for control of what is physically connected to the network. I've heard of administrators who are getting serious problems with their ethernets, who eventually track the problem down to a student with a hub in their room, or whatever.
Ethernet is (in its basic form) a shared-media broadcast protocol; everyone gets everyone elses packets as well as theirs. Zap your adapter into promuiscuous mode and there it all is. There are two basic ways around this from the hardware perspective. You either go for switched ethernet (which was traditionally been prohibitively expensive for the relatively low priority residential networks), or need-to-know hubs, which track the MAC addresses attached to each port, and scramble the data that goes to the others (for example, the 3Com SuperStack II portswitch hubs); both of these technologies have been significantly more expensive than the sort of baseline kit that has traditionally been specified in campus LANs.
Aggravating risk factors
We're seeing a lot more students running multiuser systems; Linux, *BSD, whatever. These are quite often not the best maintained machines. They are relatively frequently subjected to root exploit, and are less likely to be quickly detected as such than well run systems.
Also, the prevalence and reliance on network services is on the increase. As the density of usage increases, so increases the potential for catastrophic breaches of security. It is not unheard of for thousands of accounts to compromised by a sniffer attack from a rooted Linux box.
Why the future is rosier...
For a start, networking kit that isn't susceptible to sniffing attacks is becoming cheaper. I personally got budgetary approval to replace all our hubs with need-to-know hubs, and my successor is installing switches to service student ethernet ports.
IPv6 is on its way; hopefully bringing network layer encryption and authentication. This is the ideal solution; SSH is great, but this sort of stuff should not be going on at application layer.
There is a significantly greater awareness of the issues on the part of university technical staff. I reckon some of the security people here know more about 'r00t-kits' and 'skripts' than most of the 'kyddies'. This also trickles down into the administration: they realise its bad press to be hacked, and it's also tremendously expensive to recover from it. Coupled with the decreasing costs of doing it right, as mentioned above, it means that 'network security' is becoming a higher budgetary priority.
In summary...
The campus networks that are being installed today are probably highly resilient to being snooped, but there are a lot of legacy installations, based on equipment that's possibly 3-5 years old, that is horrifyingly insecure. Ideally, in the future, we won't have to worry about layer-2 insecurity, because we'll be protected by the IP network itself; however, in the meantime, SSH Is Your Friend!
Cheers, Nick.
Idon't mean to get alarmist, but the biggest thing that scares me about this is the fact that it wasn't a workplace, or a repressed nation, or a government agency that was approached with these "solutions" - it was schools. Campuses. Institutes of higher learning, where people go to get an education. You know, where the frontline of defense of our rights has always been held, by protest or otherwise.
Sorry, but did you even read the article? The presentation that is alluded to in the story places a strong emphasis on the rights of individuals; especially on the privacy perspective.
The point seemed, to me at least, that telnet and ftp were (for campus networks) very insecure protocols. Anyone who's ever run a packet sniffer on a shared media ethernet can testify to this. Yes, ideally all the college residential networks would be switched, or protected by Need-To-Know scrambling hubs (cf. 3Com SuperStack II PS). However, this equipment tends to be more expensive than 'dumb' hubs, and wiring of accommodation does tend to be a lower priority from the funding perspective.
We're now seeing students running Linux boxes from their dorm rooms, connected to such shared networks. We'll assume that their honesty isn't in question (however spurious such an assumption may be!); the fact still remains that such boxes are frequently ill-maintained and the subject of frequent root exploits. Once you've rooted a machine on a shared media network that runs a lot of telnet/pop/ftp, it's trivial to harvest large numbers of passwords: and don't say it doesn't happen, because I know for a fact that it does.
Given that SSH implementations are now available on most any platform you care to mention, telnet should rightly be regarded as a legacy protocol. Anonymous ftp obviously has its place, but the 'nonymous' version could easily be supplanted by SCP style functionality.
Besides, aside from physically SHUTTING DOWN the entire internet (an impossible feat if there ever was one by now) how can they protect us from ourselves, as they seem to feel they need to?
I don't get the impression that what's being talked about is 'protecting' the tech-savvie user from themselves; but rather protecting the typical user from their ignorance. There isn't a good reason to retain telnet for passworded account logins; spewing off about shutting down such services effectively being the thin end of a wedge that ends with 'SHUTTING DOWN' the internet; well, that just looks silly.
I agree wholeheartedly with the presenter's point: I'd go one step further - it's not just telnet and ftp that present the problem; IMAP and POP are also generally insecure, not to speak of the numerous HTTP-based webmail services. The solution here is less clear-cut: nice alternatives like SSH are not widely available. Roll on IPv6 and network-level encryption, eh?
Cheers, Nick.
Nice post, but I'm not sure what you mean when you say the `open source development model does directly contradict most of the software enginerring principles that are called upon in the development of trusted systems'. Do you have a specific contradiction in mind, or are you just making a an assertion about hacking culture?
I think there are specific contradictions, as well as a more general cultural problem.
From the viewpoint of specific contradictions: there is, in the trusted systems world, a certain emphasis on the importance of specification. Now, to my mind, the concept of a formal specification, and of development guided entirely by a codified specification, sits all at ease with the open source development model.
As stated elsewhere, it is the evolutionary advantages of open source development that seem to be their keenest asset; but one important thing when it comes to trusted software is getting it right, first time.
When it comes to getting it right, from a trusted systems point of view, there is also the requirement to prove you have it right. Now, I've never seen an open source project developed using anything approaching formal methods; I would be interested to be corrected on this, though!
To be still more specific, and to focus on TCSEC as a source of authority on what constitutes trusted systems 'best practice', the open source model is almost the antithesis of desirable life-cycle assurance: Orange Book calls for steps to be taken:
to ensure that the system is designed, developed, and maintained using formalized and rigorous controls and standards
This connotes everything I mentioned above, and also implies extremely high standards of configuration management and regression testing. Similarly, there is a tremendous emphasis on documentation, which I feel is a weak point for many open source projects. The level of required documentation for high assurance levels is impressive: not limited to end user documentation, but also security policy and design.
The potential incompatibility between the highest assurance levels and the open-source model is evident from Section 4.2 of the Red Book - Beyond Class (A1); here, one specific area mentioned is:
Trusted Design Environment
The TCB must be designed in a trusted facility with only trusted (cleared) personnel.
I probably needn't say much more about this.
I notice that in that brief survey, I said rather more about culture than I intended, so I'll not make any other points about that; other than to say that I also feel that many 'hackers' just plain aren't interested in doing the boring bits required for trusted systems. Despite the fact that having a DoD/NSA approved system, no-one in the open-source world has done it yet.
PS. I note your email address is in Oxford: are you a member of Roscoe's group?
No; I'm currently working on my Masters thesis, which is concerned with functional programming; I'm supervised by Richard Bird. I notice that you were an assistant lecturer at New College ... you probably know some of my friends!
Cheers, Nick.
"Trusted Software" or trusted systems in general are supposed to meet a spcification that was written by the DoD in 1983 (which was an update to docs written in the early 1970's) that outlines appropriate guidelines for access to remote systems and embedded software.
That's almost correct: at this point, you're referring to Orange Book, or DOD 5200.28-STD. It was last updated (as far as I know) in 1985. Otherwise, I agree.
However, remote access to systems is a job not only for the operating system of the host, but also for the network it runs on. Being that networks in 1983 were a little different than they are now, I would hope that a system that was meant to provide access to possibly classified data would rely on more than simply the security of the selected operating system, regardless of the openness of the sourcecode.
Orange Book is specifically about computer systems, not networks, or indeed networked computer systems. If you're interested in what the NSA/DoD has to say about networked systems, then you should probably be looking at the Red Book; aka NCSC-TG-005, which is available somewhere on the NCSC's public webserver: Radium. This server is a tremendous resource to those interested in trusted computer systems; the nice people at Fort Meade will even send you a CD containing the full website, free of charge, if you ask them nicely.
Cheers, Nick.
I originally wrote:
When you get to high levels of trust, you cease to regard testing as an adequate assurance. You want to see evidence that the system has been specified carefully and correctly, and that the code meets the specification. Needless to say, if you don't have a specification, you can't be trusted.
pallex wrote:
Yes, but this just tests that what has been specified has been coded correctly. If people are just adding bits here and there, as in an open source project, such as Linux, then nothing is specified as such, but you can test the various bits just as well. Its just outside this particular development paradigm.
If the specification correctly embodies the requirements (enter, stage left, the requirements engineers), then what you've actually proved is that the system Does The Right Thing.
I'm not sure what you're getting at when you say 'you can test the various bits just as well', if you don't have a specification. What are you going to test them against? Your personal expectations? What if another developer has subtly different expectations?
What I'm getting at, basically, is that you can't prove shit about squat unless you have some kind of specification. And unless your specification has been done in a moderately rigorous manner, then even what proofs you can do are mostly worthless.
This isn't meant as a knock to the Open Source development model, it's just a harsh fact of life. Where proof is important, specification is vital, and historically that has tended to imply Cathedral, rather than Bazaar. I would be interested to see a large open source project done with a degree of formalism. In fact, if anyone is interested in doing something that way, I'd be interested to be involved!
Cheers, Nick.
Just because something is closed source, that doesn't mean it's developed to a formal specification with formalized testing.
Absolutely true; the overwhelmingly vast majority of software (be it open or closed source) is not developed to a formal specification with formalized testing.
That said, there are pieces of closed source software which do meet these standards, and are certified to do so; examples of these include the products that the NSA (via the NCSC) certifies as part of its INFOSEC programme. The development of such pieces of software (Trusted Oracle, whatever) is reviewed, the source code is inspected, proofs are drawn up that the security policies that are alleged to be maintained are in fact maintained. In some cases, one even goes so far as to verify the object code generated.
Furthermore, what constitutes a formal specification? Both OpenBSD and Linux derive their security models from the Unix security model. That model *is* a specification. But is it a *formal* specification, and if not exactly what constitutes a formal specification?
No; the UNIX security model does not constitute a formal specification. However, one could quite easily write a formal specification for the UNIX filesystem security model; in fact, it would be quite a simple specification. Formal specifications are usually written using a mathematical specification notation, accompanied by English explanatory notes. Such specifications have the advantage that they are unambiguous, which is a tremendous advantage over English.
However, even if the UNIX security model were to be formally specified, it is an insufficient model to be trusted to any real level. It is insufficiently fine grained at one level, and it is insufficiently strict at another.
TCSEC C2 and above require the implementation of DAC - Discretionary Access Control - which requires a finer level of distinction between users' access priveleges than is really possible with the simple capability bits of the UNIX filesystem, in its original form.
TCSEC B1 and above require the implementation of MAC - Mandatory Access Control - this is all about making sure that 'security levels' on data are respected: i.e. if Joe has Confidential clearance, and I have Secret, I cannot write my Secret data into a file that Joe can read; even if the DAC system would allow me. Similarly, Joe cannot read my Secret files, even if the ACL permissions I have set would allow it.
And that's only half the story: once you have a formal specification of your system security policy, you have to prove that it is invariant. That's tricky stuff, unless you're working from a specification in which it's inherent.
Cheers, Nick.
Also, "formal spec" is a loose term. To me, the phrase "Any user can use only services they are explicitly authorized to use" is a formal spec.
Formal specification may be a loose term to you, but it is not nearly so loose to (say) the Department of Defense.
For example, for the higher levels of assurance under Orange Book (DoD TCSEC), like B2-A1, a formal specification is required that allows proof that a system does not violate its axioms. Now, your specification may baldly restate this requirement, but it does not come close to discharging a proof obligation.
For A1-level assurance, the top level specification is required to be highly formal, including the requirement for a mathematical proof of the system, and also a proof that the security policy itself is sufficient.
Least of all the ISO 9000 stuff. ISO 9000 is the least formal doc I've read in a LONG time. It's worse than useless.
ISO 9000 is a quality certification that is about process, not about the standards required of a particular project. There are, however, objective standards (which do have those letter/number names you dislike so much!) which are relevant: things like DEFSTD 00-55/56, ITSEC/TCSEC, DO-178B etc.
It seems that there is a feeling that having a formal specification is simply a hoop that some people have to jump through before getting down to hacking. This is an unfortunate attitude, and (I feel) tends to undo the whole point of making the specification in the first place.
Cheers, Nick.