Many components of systems we use have had their security properties verified up to some level. However, combining proven secure components does commonly mean that their security properties are not preserved. In a world that has become so complex that we have to break up the design in smaller parts to keep the overview, this is an interesting problem.

Combination and refinement are problematic in the world of security, as any change in the environment can have severe effects on the security. To paint the picture, one can imagine that combining a very well-secured door with an easily smashed window nullifies the security provided by the lock on the door. Of course, the window in this example is hardly secure by itself. However, two secure parts combined can also be insecurely.

Imagining Airport Security
When you are flying somewhere, you will have to pass through numerous security measures before you are allowed to board the plane. For example, you have to get your luggage scanned, the paper work will be checked and you have to pass through a body scanner. If we assume that those measures are very secure independently, we have a set of proven secure components that make up a system.

As stated, secure components can be combined insecurely. In the airport security example, the scanning of the luggage and the walking through the body scanner are separate components. This means that someone with malicious intents can sneak an object into the plane by keeping it on his body while the luggage is scanned and putting it in the luggage as soon as he passes through the body scanner. With a single action, the insecure composition is exploited to the advantage of the adversary.

Keeping Overview in Complex Worlds
The information systems of our time are very complex and large. For this reason, they are built up from smaller parts. Such a modular design allows for easier adaptation to changing requirements and it allows software manufacturers to have teams focussed on certain modules of the bigger system. Additionally, users commonly want to deploy systems for more ends than only one functionality, thereby combining software from different sources.

Software engineering came up with modular design a long time ago. In today’s world, service orientation and other networked solutions even distribute software modules over the Internet. Although this makes securing more difficult, these methods of software engineering still provide a major advantage over monolithic software engineering, where keeping the overview is almost impossible. Additionally, losing the overview also tends to influence security negatively.

Annotating for Security
At this point, we want to use modern software development methods, but also want security properties that scale with them. Given that most security properties belong to a model that precisely defines the borders of the problem at hand, this calls for a new framework for reasoning about security.

One method for secure composition works by logically annotating the modules. This means that every independent part of a system gets extended with logical formulas that describe the preconditions, postconditions and the environment invariant by which this component is secure. In that logical framework, a precondition defines the state the system should be in at the start of the component, the invariant requires what should be satisfied for the whole duration of the execution, and the postcondition describes the resulting state.

By using such a framework, one can easily evaluate if the logical formulas conflict or not. When they can be combined without generating a logical error, the components can be combined securely. This way, security evaluation can also be performed using techniques from the world of modern software engineering, which give much more room for detail.

From an Insecure Sum to a Secure Sum
As both security and modularity become increasingly prevalent in modern information systems, methods for securely combining components become more important. The introduction of a logical framework can solve this issue, although it also increases the workload by requiring the addition of logical formulas to all components. Nevertheless, this proves to be an interesting direction for modular security.

One Response to Security + Security = Insecurity

  1. Beverly says:

    I do understand what you’re getting at through the airport scanner analogy but you wouldn’t have time to sneak something into your case, given that you don’t actually get to it until you’ve already been through the body scanner!

Leave a Reply

Your email address will not be published. Required fields are marked *