Security Practice is Not Applied Security Theory, Part 2
Posted: 2011/08/11 Filed under: conceptual explanations, interesting questions | Tags: formal methods, information theory, rationalism, security, specification Leave a comment »Suppose, for the sake of argument, that security is a system property that can always be specified and implemented. Any model of security entails some notion of misuse of the system, and the very possibility of such misuse implies that the system’s basic structure, as specified and implemented, admits some kinds of use that are simply undesired. An important question is whether unauthorized use differs from authorized use in an intrinsic way, i.e. in a way that can be defined purely in terms of the system itself. Security is the problem of allowing use while preventing misuse, which means that security can be specified and implemented only to the extent that authorized and unauthorized uses can be clearly discriminated, either statically or at runtime. If security can always be statically specified and implemented, then it should be possible to construct, even if only in the abstract, ideal systems that can identify and block misuse.
Informally, a system consists of a (possibly infinite) set of possible states, together with a (possibly infinite) set of transitions between those states. Following the well-established and fairly common-sense convention of the formal methods literature, a system specification can be split into two properties: the machine property which describes how the system will function, and a supplemental property that describes any additional constraints that the system is expected to satisfy, which are not necessarily provided for by the machine property. Given a set of initial states, these two properties may be thought of as sets of paths through a directed graph that describes all possible runtime behaviors of the system. More precisely, the machine property describes the space of all possible behaviors, i.e. what the machine itself is actually capable of doing, while the supplementary property further constrains this behavior by excluding some paths in the machine property. Using this vocabulary, the question of whether security is always specifiable and implementable can be phrased as a question of whether security properties can always be reduced to machine properties, or whether a supplemental property is sometimes necessary.
Suppose that S is some system and that P is a security property that S is expected to satisfy. It is known that any property P can be written as the intersection of a safety property and a liveness property. (“The Existence of Refinement Mappings”, Martin Abadi and Leslie Lamport, 1988.) Safety describes a subset of a states in S that are allowable and specifies that execution will only visit members of this subset. Alternately, safety may be thought of as a requirement that certain states are never reached, i.e. that certain system events never take place. Liveness, on the other hand, describes a subset of states in S that must eventually be reached by any execution of S. That is, liveness stipulates that there are events in S that may not be delayed forever. The security property P is thus reducible to a joint guarantee that certain events in S will never happen, while other events in S will always happen eventually. As a consequence, S is secure if and only if certain events in the state space of S never happen, and if certain other events in the state space of S can never be infinitely delayed.
The question to answer is whether it is always possible to transform a possibly insecure system S (i.e. a system that may not satisfy P) into a definitely secure system S’ (i.e. a system that does satisfy P). As a consequence of the fact that P is the intersection of a safety property and a liveness property, S fails to satisfy P if and only if at least one of the following holds:
- There is some execution of S that reaches a state not allowed by P;
- There is some execution of S that never reaches a state required by P.
Assume that S is supplied with at least one non-deterministic input at some stage in its execution. Denote this input by x and let ! denote the set of externally provided inputs to S that may result in either (1) or (2). Since x is non-deterministic, its value can only be determined at runtime. Therefore, S can only satisfy P with certainty if the value of x is checked at runtime before any event that x might cause to transition to a forbidden state or an infinite delay.
Suppose first that (1) holds, and let F be any state in S such that if x is a member of !, the next transition will reach a state F’ that is prohibited by P. Since x is nondeterministic, S can only satisfy P in general if some state is inserted in S that checks the value of x and branches away to an error handler in the event that x is in !. Call this state G. The new state G can only ensure that F’ is never reached if it is possible to compute whether a given input is a member of ! or not, i.e. whether there is a decision procedure that fully describes the set ! of inputs that violate the security property. The question is now whether there is any set of inputs ! that cannot be described by a decision procedure on the set of inputs to S.
The answer to this question is: yes, there is such a set. If the state space of S is infinite, then any infinite subset of states that is selected from the state space by a genuinely random process will be impossible to describe as a decision procedure. A corrollary to this fact is that the quantitative difficulty of preventing the event F’ will correspond to the entropy of the set ! of bad inputs, with impossibility corresponding to the case of true randomness. For the purpose of this argument, however, the existence of a set of inputs to S that cannot be described by a decision procedure implies that, in general, G may fail to transition to either F or to an error handler, since the procedure to determine whether x is in ! may not terminate. Even if G is inserted into the execution graph of S and an attempt made to compute whether x is in ! or not, the computation may not terminate, which in turn will violate any liveness condition included in P. If G is not inserted into the execution graph of S, then some x in ! may be provided as input, resulting in a transition to F’, which in turn violates the safety component of P. If S cannot be transformed in a way that satisfies P for all possible inputs, then S cannot implement P, which means that there is at least one input x that causes an unintended or unauthorized behavior in S.
An important conclusion of this informal argument can be summarized in the following informal theorem:
Theorem (Existence of Fundamentally Insecure Systems): Given some system S and a security property P on S,
- If S takes nondeterministic inputs then S satisfies P only if there is a decision procedure for computing whether an input will violate P.
- There exists a system S and a security property P such that there is no system with functionality identical to that of S satisfies P.
It is worth noting that the fact that P is a security property is in no way essential to this argument; P could be any expressible property.
What has (arguably) been shown is that is is possible for a security property to attempt to constrain system execution in a way that is impossible to implement. A close corollary would seem to be that relative difficulty of securing a system is directly related to the information complexity (read: entropy) of the set of inputs that might cause behaviors deemed insecure. Viewing security this way, it is easy to see why, for instance buffer overflows are simple to prevent: it is always possible, and quite straightforward, to compute the length of a string. It is also easy to see why it is so difficult to prevent malicious programs from being installed on a computer: although malcious programs tend to eventually reveal their malicious intent, and some suspcious behaviors can be detected heurstically, there is no general procedure for deciding whether any given program will eventually do something harmful or forbidden.
In the prequel to this article, I made the argument that security theory and practice oftentimes seem to diverge in their respective approaches because some security problems are hard in an essential way that requires, or at least favors, a heuristic approach. The knowledge that some security properties are generally undecidable is not new; Denning and Denning showed that the detection of information leakage is not in general decidable way back in 1976. This knowledge notwithstanding, relatively little has been said about what makes some kinds of security properties hard to ensure. Traditional formal methods and security theory have usually emphasized two kinds of challenges: identifying and constructing security properties that can be decided, and designing tools and methodologies that facillitate the verifcation or at least the approximation of these properties. This focus, together with the findings above, partly explains why so many formal methods tools (e.g. Coq) are so fiendishly complex in their construction and so thoroughly unusable by non-experts; the trade-off of verifying strong assurances (e.g. decidable inference of dependent types) is a correspondingly complex and elaborate computation that is capable of excluding bad inputs. Arguably, the above findings also partly explain why security practice has come to favor patch-and-penetrate approaches: some classes of security problems (e.g. preventing unauthorized priviledge escalation) are very difficult and perhaps even impossible to enclose within a finite description. What this means is that security theory and practice tend to differ not because one is simply more reactive than the other, but because their traditional assumptions and methods tend to favor different classes of problems.
Security is an old problem and a basic problem, and has long been known to be a very hard problem as well. Relatively little attention has been paid to detailing precisely why security is hard problem, or what characterizes security breaches in general. I have tried in this space to demonstrate two facts, one unsurprising and one quite contentious: firstly, that security is basically a problem of identifying and screening a certain set of inputs to the system, and secondly that the complexity of this set gives a reliable measure of the hardness of a security problem. The existence of input sets with maximal entropy implies that there are some properties that a system can never be modified to satisfy. While this by no means implies that security is an impossible or unsolvable problem, it does indicate that there are strict limits to what can and cannot be secured against.
Security Practice Is Not Applied Security Theory, Part 1
Posted: 2011/08/10 Filed under: editorials, interesting questions | Tags: rationalism, security, specification, theoretical limits Leave a comment »What precisely does it mean for a computer system to be secure? This turns out to be a weirdly difficult and tangled question, for several reasons. One reason for the confusion is that computer security comprises a number of rather different and only loosely related engineering problems. Another major cause of the confusion is that the practical and theoretical understandings of security differ dramatically.
Security has been an active area of study in computer science for at least four decades, if not longer, and the vast theoretical literature reflects that fact. Even though much of this theory is extremely well-developed and well-understood within its own communities, it can be a real challenge to determine how security research findings have been substantively incorporated into real systems. In some cases the difficulty arises because theoretical models make assumptions that are unrealistic in practice or simply not provided, e.g. the existence of the “trusted computing base” so often assumed in papers about security type systems, without which no type system, no matter how sophisticated, can provide any assurance of security. In other cases, strong theories are so esoteric and technically challenging that it is difficult to see how exactly they should be implemented in the context real systems, e.g. the extensive work on composition of security properties, with its three-line predicates, half-page lemmas, and dense calculi .
For their part, practical systems administration and software engineering boast their own acute and well-developed lore. A number of esteemed practitioners, e.g. Eugene Spafford and Dan Kaminsky, have publicly and very vocally pointed out that most security breaches (at least, among those that are actually found out) are not the result of subtle system design challenges or the work of genius crackers. On the contrary, the bulk of security breaches seem to be the result of gross misunderstanding of basic threats and widespread ignorance of the simple countermeasures that would preclude most kinds petty snooping and ad hoc harassment. Practitioners with a masterful knowledge of a system’s ins and outs can easily spot a straightfoward defense against most kinds of attack, without the aid of a threat model or a formal semantics. The problem is that such masterful knowledge tends to be highly specific and costly to obtain. Observing the ease with which most common security breaches are prevented, the community of practitioners seems to have fully embraced the penetrate-and-patch model, where test systems are feverishly scoured for weaknesses and any security holes expeditiously plugged. While this method is effective, it is also very time- and resource-intensive, and arguably involves a large amount of duplicated work, since most attacks come through one of a small handful of vectors.
Perhaps predictably, these dual communities have focused their efforts on remediating the weaknesses of their counterparts. Theory tries to devise methods, tools, and paradigms of programming and specification that provide easier verification and higher confidence in correctness, so that systems of the future can hopefully be constructed within a framework wherein security can challenges can be better understood and more generally addressed. Practice other hand, tries to cultivate a broad knowledgebase and an active community of developers and testers that can rapidly disseminate fixes as specific problems come to light. It’s instructive to juxtapose the two apparently antagonistic views that emerge from the theory-practice duality:
- Security is a problem of understanding, specifying and correctly implementing system properties that minimize the potential for misuse.
- Security is a problem of monitoring, identifying, and effectively countering rapidly changing threats using the best available information
These two views are not inconsistent with one another, but they seem to proceed from different assumptions. Theories of security usually entail a threat model that specifies a class of attacks that designers seek to prevent. Security practices generally draw from a knowledgebase of known vulnerabilities, but assume little more than an adversary who will attack the system in any feasible way imaginable. There is a temptation at this point to label security theory as more proactive and security practice as more reactive, but besides being something of an over-generalization, such a claim overlooks the much deeper question of whether there may be a substantive demarcation between security that can be constructively specified and security that can only be understood post hoc.
I think that there is good reason to believe that differences between current security theory and practice are more than incidental, and I think that these differences are partly due to the fact that at least some problems in security are essentially hard in the sense that they have no general solution. In the next part, I will construct a small thought experiment to argue that not all secure behaviors are expressible as properties that can be specified and implemented. This distinction, I argue, is an important one, because it demarcates the limitations of formalism in addressing security challenges, and perhaps more broadly, the extent to which it is possible to lock down systems in a way that restricts their use.
Specifications Are Anti-Possibilistic
Posted: 2011/07/21 Filed under: interesting questions | Tags: formal methods, rationalism, specification, theoretical limits Leave a comment »
System specifications are basically unrealistic. The good news is that the unrealism is a very small one, and one that manifests very rarely. The bad news is that the unrealism is essential, and in that sense is impossible to eliminate. One of the essential features of computation, and of rationalism in general, is the assumption of a fixed set of unchanging truths, and it is precisely this apparently necessary feature that ties the mortal knot.
In 1988, Martin Abadi and Leslie Lamport wrote a very influential paper titled “The Existence of Refinement Mappings” . In this paper, Abadi and Lamport formalize a precise and very compelling definition of what it means for a system to correctly implement a given specification. Although the exact meaning of correctness is at the very heart of formal methods, there seems to be relatively little other work in the area of exploring the consequences and limits of correctness itself. Perhaps this is because Abadi and Lamport’s work and its close successors have already settled the matter decisively. For what it’s worth, I personally think that Abadi and Lamport’s definition is a very strong one. The stronger the definition, however, the more interesting its limitations are.
The refinement mapping method uses the concepts of state transitions and traces as seen throughout the formal methods literature from the 1970s onward. In this paradigm, a system S is a tuple ⟨Σ,F,N⟩ consisting of a set of possible states Σ, a set of allowed initial states F ⊂ Σ, and a transition relation N ⊂ Σ × Σ. A trace on S is simply an infinite sequence of states ⟨s0,s1,…⟩ selected from Σ, where each step is either a stutter, that is, a repeated state, or is allowed by the transition rule N. Intuitively, a trace on S is simply a view of what may happen when S is run. Properties of S that are used to give a specification of how S should behave are expressed by constructing sets of traces on S that should be allowed.
The above definitions above seem very innocuous, except for the fact that they involve statements about infinite sequences. An important but subtle detail of Abadi and Lamport’s work is that the property induced by a state machine such as ⟨Σ,F,N⟩ is a safety property in the techincal sense. A safety property on S states that certain states in Σ will never be reached by applying the transition function N. Intuitively, a safety property is a statement that completely circumscribes the realm of possibilities for S; in a normal run of S, only what is expressly permitted by the property can happen. The difficulty arises in defining precisely what it means for a run of S to be normal. This is not mere paranoia or trivial nitpicking; correctness is, after all, contingent upon normal operational conditions. Without a clear definition of normal operation, there is no clear definition of correctness.
An important question to ask is whether a property generated by S can ever be something other than a safety property, and what it would mean if this were the case. State spaces as Abadi and Lamport use them happen to be topological spaces, and as such, it makes sense to talk about limits. As it happens, safety properties coincide exactly with sets of traces that are topologically closed, i.e. sets that include all of their limit points. Limits in the abstract topological sense function very much like limits in the more concrete and familiar setting of differential calculus: a limit defines the value or behavior “at infinity” of some sequence of other points that is well-behaved in a very specific sense. A sequence of traces σi has a limit σ when for each m ≥ 0 there exists some n such that for all i ≥ m, the first m elements of σi are identical to the first m elements of σ. That is, the prefixes of σi successively approximate prefixes of σ, and the sequence can be thought to converge in the sense that arbitrarily long prefixes of σ can be constructed in terms of the σi. This is a reasonable definition, but it’s important to observe that the trace σ, constructed as a limit, cannot necessarily be constructed all at once: it can only be computed in terms of some initial part of its execution, with the stipulation that the remaining execution can be determined from σi.
Arguably, a consequence of this fact is that given any language for writing specifications in the Abadi-Lamport sense, there will be some system behaviors that are not expressible. (This, however, is well in keeping with what’s known about incomputability.) It also means that at least some system specifications can only be defined inductively, i.e. under the assumption that future system behaviors will necessarily conform to the rules that applied in the system’s past. More to the point, this assumption is essential to the specification itself: a specification is some set of assumptions about what system behaviors will remain invariant indefinitely.
A direct consequence of this fact is that systems cannot be realized whenever their specifications require invariance of necessarily variable conditions. Some good concrete examples come from work in hacking supposedly secure hardware: clever electrical engineers can dramatically alter a device’s function by purposefully subjecting it to physical faults. Abadi himself did some further work in this area that comes to precisely the same conclusion, namely, that specifications cannot be realized if they constrain their operating environment in an impossible way.
The title of this post makes the point very succinctly: specifications are decidedly and essentially anti-possibilistic, in the sense that they exclude large spaces of events that system designers consider sufficiently unlikely. (Note the similarity with language from real analysis, where definitions are given in terms of values that are “sufficiently large” or “sufficiently small”.) This kind of exclusion is only realistic, since it is impossible in practice (and probably in principle) to construct a system that would account for every conceivable course of events. However, the price of this realism is a specification that is unrealistic in the precise sense that operating conditions will eventually change, and thus the system will eventually fail. Considering the variability of the universe we live in, it would almost appear that specifications are so constrained that systems can only be built to eventually fail. A difficult but interesting question is whether this is a statement of grand futility, or whether it is an indication that our concepts of specification are fatally short-sighted. Phrased another way, do systems eventually fail for the precise reason that they presume invariance? Is there a meaningful definition of specification that does not entail safety?
Abadi, Martin, Leslie Lamport. “The Existence of Refinement Mappings”. Technical Report SRC-RR-29. Digital Equipment Corporation, 1988.
Abadi, Martin, Leslie Lamport and Pierre Wolper. “Realizable and Unrealizable Specifications of Reactive Systems”. Automata, Languages and Programming: 16th International Colloquium, ICALP’89. Springer-Verlag, 1989.
