Safe and Secure Software in Ada

A first installment of a booklet by John Barnes titled Safe and Secure Software: An Introduction to Ada 2005.

The purpose of this booklet is to illustrate the ways in which Ada 2005 can help in the construction of reliable software, by illustrating some aspects of its features. It is hoped that it will be of interest to programmers and managers at all levels.

It must be stressed that the discussion is not complete. Each chapter selects a particular topic under the banner of Safe X where Safe is just a brief token to designate both safety and security. For the most critical software, use of the related SPARK language appears to be very beneficial, and this is outlined in Chapter 11.

The introduction is rather amusing, so even non Ada fans may want to take look.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I found the appeal to

I found the appeal to positive vs. negative freedom an original idea. It is hight time we moved away from the B&D debates. While problematic, I think we can make some hay with this distinction.

E.g, strong typing allows you to freely experiment, and let your imagination run wild, without fear of many common mistakes. (But it also frees you from writing some kinds of units tests, so even B&D gains you "freedom from", supposedly only found in lax languages.)

Safety vs Security

I like their distinction of safety vs security. The focus on security maintaining the integrity of a system is very important, as far too many people focus on ensuring various secrecy properties. As far as I know, there is no system known to man that can adequately maintain secrecy against a determined attacker.

It's also interesting that a type system is sort of a cross-cutting tool for these ends, as it can ensure certain safety properties, as well as integrity/security invariants.

Flow Caml

Modulo out of band channels, insider attacks and such, wouldn't something like Flow Caml keep secrecy and confidentiality?

If FlowCaml can prevent

If FlowCaml can prevent covert channels, and thus prevent proxying conspirators via wall-banging, then maybe. I had thought that FlowCaml was only concerned with overt channels though, as are most security models. If FlowCaml does attempt to prevent covert communication, it must properly manage and schedule all shared resources, including garbage collection, access to the clock, and so on.

Can anyone reference a

Can anyone reference a formal definition of covert channels? My suspicion is that it is about flows that can only be described when we introduce machine or execution models, but don't quite remember where it was defined (perhaps early noninterference work?). I already see that as a strawman, so I'm curious.

I am constantly amaized at

I am constantly amazed at what I can find on Wikipedia: this.

Also, I would add that

Also, I would add that unless a covert message is perfectly orthogonal to the base channel it should produce an error rate in the base. Errors that are not readily explained could be a tip off. Also a covert message must have an implicit parse in the system. This is where the integrity of the language my make a difference. If the semantics of the language is completely defined it "should" be possible to plug such unintended holes. whatever?

1. For the Wikipedia

1. For the Wikipedia explanations:

Information theory may be from where the PL and security community nabbed the term, but somehow I think it has strayed:

"All covert channels draw their bandwidth (information-carrying capacity) from a legitimate channel, thus reducing the capacity of the latter; however, the bandwidth drawn from the channel is often unused, anyway, and so the covert channel may still be well hidden."

I may agree with the latter part (think schedulers), but not the former (again, think schedulers). In fact, solutions for preventing information flow leaks may actually further limit capacity (at least some of the older scheduler solutions).

The (outdated?) TSEC criteria seems like a construction that violates noninterference.

The eliminating covert channels blurb starts in an interesting way, but appears unsubstantiated, at least in the context of programming languages.

2. I'm not sure what you mean by an error rate or implicit parse in the system. By "whatever?", maybe you mean, who cares? This was a pretty basic question for the community given how much it has been discussed here, and as a language and systems builder, understanding it better would be useful for deciding how to factor it in to future work (worth the effort? how much? in what way? etc).

As a light stab at it, I'd view the program as one agent, and an opponent interacting with the program (providing input and running it) as another. A leak exists in a program if there is some agreed upon predicate that an opponent should not be able to discern by operating the program. The defender, given this predicate, may modify the program under some rule system (say have it guarded by a type checker, monitor, etc) -- a covert channel exists if the leak still exists. Thus, by covert, we mean beyond the body of knowledge of the defender with respect to judging whether the opponent can deduce the predicate.

I would also disagree with

I would also disagree with the sentiment that all covert channels draw their bandwidth from a legitimate channel. Consider power analysis attacks; I haven't heard anyone argue that the amount of power consumed by a circuit is either a legitimate channel or detracts from the bandwidth of a legitimate channel.

As far as language based security models that include covert channels, I seem to recall finding ones that do a fine job of finding covert data channels (those channels that depend on the value of state or the order of state transitions), but not covert timing channels (those channels that depend on measuring the duration between events).

If the semantics of the

If the semantics of the language is completely defined it "should" be possible to plug such unintended holes. whatever?

This is not the case. Here is a brief overview of real covert channel issues in languages. Basically, any shared resource is a potential covert channel. To attenuate the bandwidth of such channels, use of a resource must be properly scheduled and accounted for, with sufficient overheads as to make wall banging/listening infeasible. No existing system accomplishes this, though Mark Miller's E performs some limited attenuation to this end. Mark himself has serious doubts that covert channels can be eliminated completely.

Still, we haven't even nailed the overt channel problem, so covert channels aren't that big a deal at the moment. This thread has two main points though:

1. Security is not about secrecy.
2. Information flow systems cannot adequately prevent information leaks.

We should be realistic about the achievable goals, lest we start relying in security properties which don't actually hold in the real world.

I don't get it. Your linked

I don't get it. Your linked example is specifically about a "semantic hole" as I would define it. The ambiguous definition of hashcode().

It's unknown whether covert

It's unknown whether covert channels can ever be eliminated. Which is the whole point: restricting information flow is probably impossible, so the whole "security == secrecy" association is bogus. Computer security is mainly about integrity, not secrecy.

How can you hope to

How can you hope to eliminate something that you have not defined?

Your response hints you believe there is a clear relationship between information flow and covert channels. Can you define either? I know how to define particular information flows, but the general case, for either?

The more I think about it, it seems that my beef is with the connotation of 'covert', where I interpret it to be beyond what we can analyze (once we can check for it, it is no longer covert). However, after my previous response to Hank T., I think something else is actually meant (in the information theoretic sense): a program is meant to give exactly a certain output, and if it provides anything more, it must be an acceptable leak. This implies a specification of functionality and an implementation (meant vs does), and a policy (acceptable leak).

[Edited for formatting - stayed up late =/ ]

I'm not sure about formal

I'm not sure about formal definitions, but you're getting close with your specification of program behaviour. Covert channels are only of interest in the presence of malicious programs though, so specifications are hard to come by. The way I see it, a covert channel is any information channel which was not explicitly authorized (ie. not an overt channel). Perhaps there is a more formal treatment elsewhere. I have been meaning read up on some more information flow literature, such as Type Based Techniques for Covert Channel Elimination and Register Allocation, and Language-Based Information-Flow Security.

For an example of an actual exploit using a covert channel, see the Darpa Browser report. This was a security audit of a simple web browser written in E, which could safely run malicious HTML renderers. I'll quote the relvant section:

Exploit
Transmission of user's page through a covert channel: By using its ability to allocate RAM and consume CPU resources, the renderer could engage in "wall banging": forcing system performance to rise and fall in a pattern that can be analyzed, from which data can be extracted. A conspiring caplet, loaded and running at the same time as the renderer, could extract this data by “wall listening” and use its own capabilities to further transmit the information.
Outcome
All known practical security systems are subject to such covert channel “wall banging” attacks, and the best limitation normally attempted is to limit its bandwidth. E addresses instead the other half of the problem, where a true solution is indeed possible. For the conspiring caplet to read bits from a covert channel (to “wall listen”), it must have access to a clock or some source of non-determinism. The web browsing caplet described here cannot wall-listen because it does not have such access.

CPU caches are also covert channels in the same way. Malicious code could engage in certain memory access patterns to affect system performance to transmit data. Such channels are so fundamental to many systems, that I find it very unlikely that we will ever close them all. Thus, security cannot meaningfully be about secrecy, it must focus mainly on integrity. That's where all of our modern security problems are anyway.

CPU caches are also covert

CPU caches are also covert channels in the same way. Malicious code could engage in certain memory access patterns to affect system performance to transmit data. Such channels are so fundamental to many systems, that I find it very unlikely that we will ever close them all. Thus, security cannot meaningfully be about secrecy, it must focus mainly on integrity. That's where all of our modern security problems are anyway.

The channel isn't just the CPU cache, though - the CPU cache is the transmitter and the clock is the receiver (unless you're providing an API to read cache fault counters). I agree with your quote that blocking the receiver is much easier than blocking the transmitter in this case. Why don't you consider this a viable solution?

I don't think this is ad hoc. When you send a message over a network, the information transmitted is the payload + the time. In general for other resources we can define an API such that information obtained through the API depends deterministically on only the calls made in a particular process + any overt communications that the resource is exposing. I can see this requiring care to setup and validate, but it hardly seems impossible.

Also I don't think it's fair to say that secrecy isn't a modern security problem. I assume you just mean that secrecy is not where most attacks are directed right now, but the problem is ubiquitous. I imagine as soon as you plug the integrity holes, though, the secrecy holes will be exploited. And there are some recent examples, like spam with embedded picture links that verify delivery to the sender.

Why don't you consider this

Why don't you consider this a viable solution?

I don't think restricting the clock from all potentially malicious code will be viable. How many of the programs you run give you bandwidth stats, or other sorts of stats computed from clock time. I bet there's a decent amount of such code. You don't want to have to trust all of it. And the clock is but one channel. Any shared resources which have been optimized for performance reasons, like caches, are potential channels.

Also I don't think it's fair to say that secrecy isn't a modern security problem.

I never said secrecy wasn't a problem, just that it shouldn't be considered a computer security problem. I know, seems heretical. :-)

I think security should largely be about maintaining a system's integrity.

I assume you just mean that secrecy is not where most attacks are directed right now

That is also another reason to focus more in integrity: without integrity, secrecy is probably impossible.

the problem is ubiquitous. I imagine as soon as you plug the integrity holes, though, the secrecy holes will be exploited.

The secrecy holes seem simply too numerous to count, and I doubt they will ever be adequately plugged. Perhaps the information flow literature knows something I don't though.

And there are some recent examples, like spam with embedded picture links that verify delivery to the sender.

I don't see how this is an exploit enabled by secrecy. If anything, it looks like an integrity hole, where the mail renderer somehow obtained network access without permission.

A secrecy exploit was this SSL vulnerability vulnerability where the private key could be extracted by a timing attack.

Ok, so it sounds like partly

Ok, so it sounds like partly you're just arguing for a particular definition of 'security'. I actually don't care what the definitions are very much, but I think that excluding secrecy conflicts with common usage.

The secrecy holes seem simply too numerous to count, and I doubt they will ever be adequately plugged. Perhaps the information flow literature knows something I don't though.

Starting with an API for a modern OS and trying to 'plug the holes' may very well be difficult, but designing from scratch an API that doesn't leak should be comparatively easy. Of course this API will preclude certain optimizations, and in some cases may even be incompatible with existing hardware.

Ok, so it sounds like partly

Ok, so it sounds like partly you're just arguing for a particular definition of 'security'. I actually don't care what the definitions are very much, but I think that excluding secrecy conflicts with common usage.

To a certain extent. It is a definition more in line with that used in capability security circles. With capabilities it's very hard to prevent delegation and impede information flow, but in reality, you actually can't impede that anyway (even just using overt channels, as agents can just proxy access). One thus conludes that integrity, not control of information flow/secrecy, is a more important security property.

Starting with an API for a modern OS and trying to 'plug the holes' may very well be difficult, but designing from scratch an API that doesn't leak should be comparatively easy.

I don't know about easy. As jeff_marshall notes above, it all depends on the scope of your model. I doubt very much that a model will ever encompass all relevant channels and maintain an acceptable level of platform independence. I'd like to be proven wrong though.

As jeff_marshall notes

As jeff_marshall notes above, it all depends on the scope of your model.

I agree and I should have clarified what I was suggesting: I think it is possible to design a set of APIs for capabilities such that the only communication possible between isolated processes are through the overt ones laid out in the API.

I would also agree that trying to stop covert information flow through overt channels is a very difficult problem (e.g. trying to prevent stenography). So it seems like a reasonable approximation to assume that all information leaving an untrusted process could be disclosing any secret of which that process has been made aware. If you can prohibit covert communications between processes (which I contend is not as hard of a problem), then you can still give sensitive information to an untrusted process and forbid it from communicating with processes/resources that can disclose information. So I could download a web app and use it to work with sensitive financial data or something.

I agree and I should have

I agree and I should have clarified what I was suggesting: I think it is possible to design a set of APIs for capabilities such that the only communication possible between isolated processes are through the overt ones laid out in the API.

But this is exactly counter to the argument that jeff notes (I think), namely, that even if no overt channel existed at the semantic level, a covert channel can be established since two supposedly isolated processes run on the same machine with shared resources, like caches, clock, etc. A language authorizing only overt channels is easy, but it doesn't necessarily forbid such covert channels since they are established below the language's level of abstraction.

The exploit I linked to wasn't even on the same machine! Can't get more isolated than that, but it uses similar techniques to infer server-side state from timing delays.

I agree about the low likelihood of detecting steganography over overt channels, but I don't consider that an interesting case.

So I could download a web app and use it to work with sensitive financial data or something.

Honestly, I don't think you can never be 100% certain of that, due to the possible covert channels between conspirators that we've been discussing. You might run that web applet on sensitive data with no network access, which wall bangs for another useful program you're using which does have network access.

Even assuming a very noisy covert channel of 128 bits/sec, which is incredibly low, it would take less than 10 seconds to leak an RSA private key.

naasking gets the point I

naasking gets the point I was trying to make. For many systems, building a correct model to evaluate the presence of covert channels can be daunting.

Take AES, for example. During the NIST contest, lots of smart, trained cryptographers overlooked the fact that a table lookup might not be a constant time operation. Rijndael, which uses a table lookup whose index depends on the secret key, won the contest. Daniel Bernstein then publishes a clever attack against implementations of Rijndael on CPU's with data caches leveraging differences in encryption time due to that table lookup.

Covert channels are an arms race: as soon as you block the channels you know about, somebody discovers a new one.

Excellent example! There are

Excellent example! There are some covert channels that can be eliminated with high confidence. I recommend the cap-talk thread I posted about here.

These are all the same

These are all the same attack though: do something that subtly changes system performance somehow and then detect it by measuring time differences. Trying to prevent information leaking out of the system seems hard, but keeping that information from leaking back in to certain isolated processes seems much easier.

The types of restrictions that would need to be put into place on reading the clock or on the timing of outgoing network operations would no doubt be annoying, but I don't think they'd be a show stopper as limitations applied to untrusted code downloaded and executed without any user knowledge or consent.

naasking wrote: I don't know

naasking wrote: I don't know about easy. As jeff_marshall notes above, it all depends on the scope of your model.

Quite. Just think about the headaches differential power analysis has caused smartcard designers. I doubt that real-life security can be modelled with anything much short of a physics simulation.

Interesting idea. Perhaps

Interesting idea. Perhaps future compilers will include a physics model of the target CPU to perform such analyses.

Not enough

Simulating the physics may be necessary but not sufficient. Information defies a reductionist account, and higher levels above physics will also have to be simulated and accounted for.

physics unnecessary

Power attacks imply the ability to read power levels; restricting inf. flow from hw perf. monitors to software is simple (modulo timing attacks), and we often assume nodes in which there is physical access are already corrupted.

Do these assumptions imply we do not need a super fine grained physical model? I'm fine with special casing smart cards, and further simplifying security, new architecture designs often feature physical resource partitioning. Can we cover large classes of important applications without throwing our hands in the air?

TEMPEST

The existence of the TEMPEST spec should tell us that eliminating power analyses is not so easy.

That's a red herring.

That's a red herring.

Higher-order reasoning

I'm guessing that physical simulations specified in a first-order framework are likely to have problems with defining information flows, but these will go away if we allow higher-order reasoning.

How can you hope to

How can you hope to eliminate something that you have not defined?

The input function(s) of a program are a simple parse. They are so pervasive and so common that we probably ignore them. But these functions amount to an unintended definition of both intended and unintended messages. Correct parsing should unambiguosly recognize correct messages and reject all others as errors (or covert) as the case may be. After all this there is the possibility of a perfectly orthogonal covert message, But for this message to "get through" there must be an orthogonal parse. This is unlikely unless it has been designed in or planted as a virus.

Add to this the tendency to ignore errors all together and you have a prescription for trouble. Buffer overflow attacks apparently don't produce errors until the crash occurs. The errors start long before that.

"Whatever" only means that it is complicated and there are lots of good and different points of view.

This is a interesting link

This is a interesting link that illustrates both the problem and a possible cure. Two cooperating parties can always communicate secretly over an open or base channel. This seems to be a fundamental property of languages and communication. Real security would need to assume that this is always possible. There is nothing about language or computer language of any kind that could prevent this and so it would seems to me to be a waste of time.

Edit: The problem is unauthorized, or not permitted communication between cooperating parties. This is actually a legal right unless prevented by contract. For example my identity is protected by PayPal, but nothing prevents an insider from leaking that information. PayPal probably prevents that by contracts with it employees. So far it seems to work but I keep a minimum balance in my account anyway.

That's a pretty good read.

That's a pretty good read, and a working covert channel. This echoes exactly what I was saying above:

The virtual memory machinery would have to do extra bookkeeping and extra page reads. To close the CPU demand channel, the scheduler would have to preallocate time slots to higher levels, and idle instead of making unneeded CPU time available to lower levels.

This is an example of what I mentioned above: efficiency is the friend of covert channels. In order to reduce covert bandwidth, you have to account properly for shared resources, and reserve additional "idle" time instead of immediately switching to the next task. Basically, you're wasting resource time/bandiwdth so that it can't be co-opted for covert communication.

I finally found one of the interesting threads on cap-talk discussing how to attenuate or eliminate certain covert channels. There are about 5 or 6 posts in that thread well worth reading.

[Edit: sorry, the thread was on e-lang, not cap-talk. Most of the same people participate on both lists though.]

Current systems that run

Current systems that run thousands to tens of thousands of threads normally use SIMD and SIMT synchronization; I disagree with the claim about efficiency being the friend of covert channels. (More specifically, many current notions of 'efficient' are outdated in these models and hardware trends point to them). While the critical path, which exposes timing etc attacks most often, remains an issue in such systems, it's at most a secondary concern. Not to claim programs run over massively parallel architectures are not susceptible, but what I've seen from the architecture folk, we'll have a lot more control and information with respect to power and time, and parallel execution of hardware threads, even when they have different paths, is often still run in lockstep.

Further, I think the interesting case of covert channels is for security, which means there is no cooperation (so collusion of multiple agents, sure, but they can be modeled as one); it's a cat and mouse game.

Looking forward to the reads after some more hacking, however :)

Chapter 1, Safe Syntax

Required vs. optional

One thing that bugged me about it was that some of the touted things are optional e.g. named arguments. I guess when I hear somebody talking about safety, I sorta hope that it will be more dictatorial so that you avoid having crappy code more easily enter the source base. I mean, you could do a super hacky maybe vaguely similar thing in C by requiring all functions take structs representing their arguments, no? OK maybe not, but e.g. Perl allows named args and that isn't all that exciting where I suddenly think Perl is great for safety. By which I only mean that for me personally to see something as really striving to be "safe", it has to be a lot more anal overall.

Ironic

Ada is usually portrayed as being too dictatorial... It's amusing to see it critiqued from the other direction.

More seriously, Ada provides enough language-level support for many of these things that most compilers provide switches allowing you to mandate coding style depending on your particular needs. This allows you in general to be as strict as you want or as lenient.

Chapter 2, Safe Typing

Chapter 2, Safe Typing

[Edit: Fixed Linked. Thanks]

Chapter 3, Safe Pointers

Chapter 4, Safe Architecture

Chapter 8, Safe Startup

OTish

anybody know of anything like Lisp-flavoured-Erlang but for Ada? :-)

It depends of what you mean

It depends of what you mean by that. If you are willing to accept a system that is statically typed, does not support first class functions, and is limited to a fairly small number of concurrent processes, than Ada is Erlang...

sorry -- i meant a lisp-sexpr focus, not an erlang focus

i was just wondering if i could get s-exprs instead of ada syntax, so i could then also have macros and stuff. tho it would presumably have to look more like Typed Scheme. for some reason i get a kick out of things like LfE or Liskell.

Trivial

First off, you can have macros with Ada syntax; there's nothing magical about s-expressions.

Adding an s-expression syntax over Ada would be an easy exercise.