Correct By Construction

This post is part two of our series about secure software methodologies. Check out the previous post here.

When it comes to construction, design and security both matter. If a building were designed only to be strong it would be short, wide, and made entirely out of rebar concrete. That building would be pretty likely to survive any host of natural disasters- and would be a great hideout in a zombie apocalypse! But what if that building was meant to be a daycare? Sure, we want a daycare building to be strong and protect bumbling babies from storms (and the undead). But a building designed only for strength is going to be cold, dark and pretty dreary. A rebar concrete building is a perfect solution for a bunker… not so much for a nursery. The building might be safe, but it’s not particularly useful.

Security is critical, but context matters.

Good construction requires both good design and appropriate security attributes at each level of a system (or daycare building, in our example above). Above all, a system must be useful. In other words, security is critical, but context matters. Building secure software requires a series of design tradeoffs throughout the development process. These choices allow engineers to build useful systems that balance many competing priorities- security, performance, reliability, cost, and more.

Start With a Strong Foundation

The theory of secure software has a basic tenet: Secure software does what it’s supposed to do, and NOTHING ELSE. Managing the assumptions and guarantees of each function and component in a complex system is a daunting task. At Tangram Flex, we firmly believe that the best and most efficient way to create secure software is to ensure that it is correct by construction.

Constructive techniques require a developer to build security into each level of a software system. A successful method to building secure, correct software systems follows five basic steps:

1. Create a modular component architecture
2. Implement functionally correct code
3. Harden interfaces between components
4. Implement system-level security
5. Evaluate and iterate

These methods begin with building a model of a system’s software components to use as a guide for construction. In this series, we will walk through the steps above and explain the practices for creating secure, correct software components and systems.

Demolition Day

The first step to creating secure software systems is to create a modular component architecture. Software construction should begin with three basic steps:

1. Decomposing system-level requirements into granular functions
2. Allocating each function to a software component
3. Documenting the decomposition and allocation in a system model

This process creates a modular component architecture where every component represents a function of the system. This is where it gets fun- now that each of the system’s components are identified, we can apply decomposition again. Each of the system’s components should be decomposed to a point that allows us to identify the inputs and outputs of the component’s related function.

A Little Bit Goes A Long Way

We’ve learned a lot about creating modular architectures over the last couple years at Tangram. Some modeling experts push engineers to model software behavior all the way down to individual functions and threads to achieve any utility. In our experience, it has not proven necessary or even particularly advantageous to try to model every aspect of a system. Most software developers will never see a return on the time and effort it takes to model and maintain a system down to this microscopic level.

In every project we have taken on, we have found that models are usable and scalable when they contain only the information needed to capture relevant behavioral interactions between software components.

At a minimum, a good model includes the properties associated with assumptions and guarantees between components and explicit ties to software. Modeling too much information is actually worse than too little. Our experience shows that increasing the amount of data present in the model means that some data will not be updated regularly. This means that some data will be stale (often with no indication to the user), reducing trust in the overall model as users rely on old, outdated information.

Paving the Happy Path

Why do we do this? Well, let’s think back to the idea of an assume-guarantee relationship like we talked about in The Theory of Secure Software. An assume-guarantee relationship is a simple way to evaluate the functional behavior of the software component. If the assumptions and guarantees are too complicated, we can’t build a good model. The component needs to be decomposed to a level where its inputs and outputs can be identified confidently. This level of understanding allows engineers to construct assume-guarantee relationships that help them understand that a system will function properly and users will never experience any unexpected behaviors.

The happy path to secure software is paved with iterations. The proper level of decomposition will likely take a few rounds of analysis. The most important thing to know: a successful assume-guarantee relationship is one in which the assumptions and guarantees about each software component can be evaluated through test or code analysis outside of the model.

Signing the contract

Like a building construction project, continuing to the next steps in a correct by construction plan requires a contract. In our case, the software components, their functions, and the assume-guarantee relationships they carry create a system model. Its critical term is this:

The final software component will produce the guaranteed output as long as it receives the assumed input.

This model is a contract between the systems engineer and software developer with the following expectations:

• The Systems Engineer has built a model that both addresses all system-level requirements and defines functional requirements with assumption-guarantee relationships
• The Software Developer will understand the assume-guarantee relationships and create software to satisfy the functional requirements of the component model
• All code provided by the Software Developer will be graded against the model

The model, like any contract, is the final source of truth. If either party disagrees about the assumptions, guarantees, or component behavior, the contract must be renegotiated. The model itself must be updated, and all test requirements and code must be graded against it.

Putting Up The Walls

It’s time to get to work. Check out our next post in this series where we will talk about what it takes to build a truly secure system. Follow Tangram Flex on Twitter and LinkedIn for the latest.

Adapted from a paper written by Don Barrett, Systems Engineer at Tangram Flex

Edited by Liz Grauel, Technical Writer at Tangram Flex