Remember me

Separate lives

Published on 2 March 2009

Search the magazine archive





By Chris Edwards

Soldiers standing next to a helicopter on a warship

To get more peace of mind, military users are turning to formally proven software to save operating systems from themselves.

Colonel Bud Jones is not having a quiet retirement. When he stepped down from a command role in the US Army, he moved over to the US Central Command to take part in a programme that will see the US military overhaul its computing and communications infrastructure.

As subject matter expert for US Central Command, Jones is trying to help prevent the electronic sprawl that now dogs military operations. The armed forces have to deal with much more complex situations than before; for example, in Afghanistan and Iraq, the US is fighting alongside and sharing information with coalition troops that were on the opposing side not so long ago. “Is the enemy of yesterday a friend today?” asks Jones.

Many of the partners in a conflict want to share data, but every nation will inevitably deem some data too sensitive to share. As a result, a number of machines will sit on one network with a lower level of security while others – classed as secret or top secret – are attached to a much more secure network.

It’s not possible to hack into one system from another, simply because there is no connection. The ‘airgap’ is the most advanced security measure today’s armed forces use to ensure that a break-in on one networked system does not affect another. The problem is that the same people have to be able to use both types of system, and they may be faced with as many as five different computers – none of which are physically connected – in a working day.

The users are required to log off one system, walk to another – which may be in a different tent or office – and then log on to it.

“Today’s network frustrates people because they have to get from one network to another. They have to remember all their different passwords, and we force them to change their passwords regularly,” says Jones.

Embedded systems

The problem is not just one of inconvenience to individual operators. There is the time lost in getting vital information, such as troop movements, from one coalition partner to another. And then there are the logistics. If you have to ship four times the number of computers, network switches and cabling to a forward position, you are tying up helicopter and cargo-plane capacity that could be used for food, ammunition and other supplies. As a result, the problem of moving IT equipment around slows operations down.

“What we are looking for is a single infrastructure connected to a single wire and to remove the airgap,” claims Jones. “We want information where it is needed to give access to coalition data from their desktops. What today is physically separate we want to put together virtually.

“What we are doing today is expensive. If we can consolidate to a single box and wire, we can save a lot of money.”

The answer for Jones and his colleagues looks as though it will come from the world of embedded systems, an environment that uses much smaller code bases than those used in desktop IT. This in turn makes it possible to meticulously check the software for holes and even formally verify. On their least secure systems, the military may well still run conventional operating systems, such as Microsoft Windows.

“At the Department of Defense, we say we have to have Microsoft and we are not going to change,” argues Jones.

But, underneath, a kernel monitors access and ensures that the Windows portion does not see the applications running in a dedicated, secure part of the system. It’s taken a while to get to this stage.

John Rushby, then working at the University of Newcastle-upon-Tyne, introduced the idea of a separation kernel for improving computer security in a 1981 paper presented at the Association of Computing Machinery’s Eighth Symposium on Operating System Principles. The paper argued that a formally verified kernel “is widely considered to offer the most promising basis for the construction of truly secure computer systems, at least in the short term”.

In practice, ‘short term’ meant more than 20 years. But, in the early 1980s, Rushby recognised there was a problem with traditional methods of enforcing computer security using standard operating-system designs. “Current approaches to kernel design and verification developed out of concern for the problem of providing multilevel secure operation on general-purpose multiuser systems – whereas many of the present-day applications which require some form of guaranteed security are special-purpose, single-function systems,” Rushby wrote. “Attempts to support these applications on a conventional kernel have led to systems of considerable complexity whose verification presents difficulties that are quite at variance with the evident simplicity of the task which the system is intended to perform.”

The answer is to put a security kernel in charge and run a bunch of operating systems on top, each with its own defined purpose and security clearance. No application in one domain can talk to one running in another domain without going through the separation kernel, unless the system is designed to allow that kind of communications. The approach is not dissimilar to virtualisation, in which guest operating systems run under a hypervisor that controls access to the hardware. Operating system vendor Lynuxworks plans to have its own hypervisor certified as a separation kernel, adding functions to perform the security checks to messages that pass between domains.

For its part, software supplier Green Hill is using a certified version of its Integrity-178B kernel, used in aerospace systems, as a separation kernel.

Less secure operating systems will run on top of the kernel each in separate spaces managed by an emulation layer: the Padded Cell software in Green Hills’ case. Lynuxworks claims using a hypervisor will provide higher performance than emulation. However, proving secure operation will involve detailed knowledge of how the virtualisation features inside the microprocessor work.

The search for EAL 7

With operating systems running under emulation or in virtualised partitions, instead of having to separate those systems with an airgap or dedicated secure-networking equipment, it becomes possible to collapse everything onto one piece of hardware. In principle, it will solve one of Jones’s biggest headaches. As Rushby wrote in 1981: “The purpose of a security kernel is simply to allow such a ‘distributed’ system to actually run within a single processor.”

A version of the Integrity-178B operating system running on a PowerPC processor was certified by the US government’s National Information Assurance Partnership (NIAP) – organised by the National Institute of Standards and Technology (NIST) and the National Security Agency (NSA) – to Evaluation Assurance Level 6+ last autumn. The previous record holder was the STOP operating system sold by BAE Systems, which was certified to level 5.

Some vendors have claimed to have operating systems that they believe could be certified to the highest level, 7, but none has done so as yet. Founded in 2001, Aesec bought an operating system from Gemini Computers that is meant to be able to pass EAL7, but no one has taken it that far yet. LynuxWorks hopes to be the first with an EAL7 certification for its LynxSecure product, but has yet to begin the evaluation procedure. Wind River claimed to have started to work on getting its Safety Critical ARINC 653 product certified to EAL 7 in  2004 in conjunction with Smiths Aerospace. However, the product has not yet entered evaluation since the announcement was made almost five years ago and Wind River declined to comment on whether it had made any progress towards launching an evaluation.

Steve Blackman, director of business development for aerospace and defence at Lynuxworks, says the company expects start evaluation this year, possibly on more than one project. He claims the product is ready but that the way in which the certification process is set up means that a vendor cannot take a product through on its own. To be able to certify above EAL 4, NIAP has to enlist help from NSA experts – a resource that can only be justified if the agencies are satisfied that the project is worthwhile. In practice, it means having a sponsor.

“The way it works in the US, to be evaluated you have to be sponsored by a programme. You used to be to able to just submit yourself. But we have a few programmes taking us through the evaluation process,” Blackman explains.

Too secure?

As the first company to succeed in getting an operating system approved to one of the highest security standards possible, Green Hills aims to make the most of its position. The company is so confident that the idea will prove fundamental to IT security among commercial users that Green Hills has created a subsidiary to sell to organisations such as banks and industrial users.

Blackman says he has doubts about the applicability of EAL 6+ or 7-rated software outside the military and avionics areas. “The requirements are very stringent and the constraints on using the system are very high. They are more stringent the higher you go up and that puts restrictions on your systems. Can you open a door with just one key or do you need a key and four padlocks? High assurance is possible in a highly restricted world.”

Dan O’Dowd, president of Green Hills, asks rhetorically: “Is EAL 6+ too secure? We can dial in whatever level of security is required.”

By letting people run their existing operating systems, such as Windows, but prevent them from accessing sensitive areas on the same machine, Green Hills hopes it can encourage people to gradually harden their systems. Over time, they might shift critical routines, such as Secure Sockets Layer (SSL) encryption for web services, kept in a less-secure operating system to be managed by the secure kernel itself. By adopting the Posix programming interfaces, that job should be made easier.

Although LynuxWorks is more sceptical of the general applicability of high-level EAL-certified operating systems, the company is planning for a similar migration of function. “This ability to take legacy code that wasn’t in a security environment and migrate it into secure bits of hardware will be a key factor,” says Day.

In the meantime, Jones and colleagues are pressing ahead with the single-machine plan. “I asked the question: can we do this on a LAN? Green Hills came back and laid out a proposal. We are sponsoring a joint technology demonstration called OB1,” he says, adding that the name “gets everybody’s attention”.

“What’s the payoff? Instead of having to load ships with four lots of equipment and wire, you just ship one. You save on cost and ship stuff quicker. Central Command has about 35,000 users spread over five networks. We can avoid a cost of $200m using this solution, so we are very interested in this going to fruition.”

A lot of other users in the military and elsewhere will look at the programme and ask the same question: can you help us, OB1?



Comments

All comments

You need to be registered with the IET to leave a comment. Please log in or register as a new user.

Toolbox

Comment on this article

  • Box out

    The road to assurance

    Getting to a rating such as Evaluation Assurance Level (EAL) 6+ or 7 is not a simple process, especially when you have a ‘plus’ involved in the process. Roughly speaking, the EAL number increases with better security, as determined by the Common Criteria standard, which was introduced internationally in 1999.

    However, the number is not enough on its own to describe what the product actually passed. The detail is held in the Protection Profile: the EAL just tells you to what level the product has been designed and tested.

    The Protection Profile determines the requirements for a given product, whether it is an operating system, firewall, hypervisor or something else. In the case of Green Hills’ certificate for Integrity-178B, the profile was determined by a June 2007 document “US Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Version 1.03”. The Security Target defines the security requirements a product has to meet.

    It gets more complicated. It is possible to bolt on other functions to a Protection Profile and then have that evaluated. This is where the plus-sign comes in – it shows that there are additional requirements that have been tested. And, as you go up the assurance levels, the types of test and verification change.

    Robert Day, vice president of marketing at Lynuxworks, explains: “As you go up through the common criteria levels, when you get to 6+ and 7 you have to have formal methods to show that the operating system does what the operating system is designed to do, rather than going through and making sure there are no holes in it.”

    Because of the requirement for formal verification at EAL 7, LynuxWorks started from scratch when developing a version of LynxSecure that the company could put forward for EAL testing.

    “We used a methodology of correct-by-construction, using formal methods from the start,” says Steve Blackman, director of business development for aerospace and defence at LynuxWorks.

    Working to EAL 6+, Green Hills and evaluation partner Rockwell Collins was able to use a semiformal verification process, with some novel techniques developed by the aerospace company to match a formal specification to the original operating-system code.

    Raymond Richards, principal engineering manager at Rockwell Collins’ advanced technology centre, says: “There are two different tacks to using formal methods. One is correct by construction. You model and prove whatever you want to prove and then develop the system from that model. We took a different tack: modelling something that was already there.”

    The team developed formal modelling techniques that would allow them to build formal proofs that had a similar structure to the code, making it easier to demonstrate the match. “We used syntactic sugar to make the model look as much like C or another imperative language as much as possible,” Richards explains. “There is no other operating system that has been evaluated with this degree of rigour.”

  • Threat levels and protection

    T1: Inadvertent or accidental events (such as tripping over a power cord)

    T2: Passive, casual adversary with minimal resources who is willing to take little risk (such as listening)

    T3: Adversary with minimal resources who is prepared to take significant risk (such as unsophisticated but determined hackers)

    T4: Sophisticated adversary with moderate resources who is willing to take little risk (such as organised crime, sophisticated hackers and international corporations)

    T5: Sophisticated adversary with moderate resources who is willing to take significant risk (such as international terrorists)

    T6: Extremely sophisticated adversary with abundant resources who is willing to take little risk (such as a well-funded national laboratory, nation state or international corporation)

    T7: Extremely sophisticated adversary with abundant resources who is willing to take extreme risk (nation states in time of crisis)

  • Levels of assurance

    EAL 1: Functionally tested

    Applicable where some confidence in correct operation is required, but when threats to security are not viewed as serious.

    EAL 2: Structurally tested

    Applicable where a low to moderate level of independently assured security is required in absence of an available development record. An example is securing legacy systems or cases where access to the developer is limited.

    EAL 3: Methodically tested

    Allows a developer to gain assurance from security engineering at the design and applies where a moderate level
    of independently assured security is required.

    EAL 4: Methodically designed, tested and reviewed

    Applicable where a moderate to high level of independently assured security is required for commercial products and where developers or users are prepared to incur additional security-specific engineering costs. It is the highest level at which it is likely to be economically feasible to retrofit to an existing product line.

    EAL 5: Semi-formally designed and tested

    Requires rigorous commercial development practices supported by the moderate application of specialised security engineering techniques.

    EAL 6: Semi-formally verified design and testing

    Applies security engineering techniques to a rigorous development environment and is for security products that will be used in high-risk situations

    EAL 7: Formally verified design and tested

    Applies to products to be used in extremely high-risk situations or when the high value of the assets justifies the higher cost. Realistically, it is limited to products with a tightly focused set of functions that are amenable to extensive formal analysis.