Jul 2016

Verifiable software


Principal Consultant of L-3 TRL Technology, Paul Yates, explains why scalable, verified HG software is the only solution capable of addressing the increasing complexity of IT – from elaborate enterprise-scale networks down to small internet of things devices.

The issues

The government systems of the future will require software implementations to address the challenges brought about by the growing complexity of their IT systems.

These challenges include:

•            Complexity/scalability: The future is hyperscale: ‘born-on-the-web’ hybrid clouds hosted on homogenous hyper-converged infrastructure appliances. CATAPAN can’t scale to match the future inter-datacentre (north/south) throughput of the government portion of the imminent zettabyte internet.

•            De-perimiterisation: Current products rely on a security critical barrier at the perimeter, usually implemented in hardware. This perimeter is disappearing.

•            Rich services: The increasing intricacy of ‘rich’ services is leading to increasing bypass complexity, such as migration.

•            Speed of development: The pace of change is outstripping the traditional cycle of development, validation, evaluation and accreditation.

•            COTS platforms: Commercial off-the-shelf systems such as SGX/Trustonic have many good IA properties.


The answer

Scalable, verified HG software is the only answer, hosted on both trusted platforms and semi-trusted commercial (COTS) platforms.

The changes require a new paradigm in HG/HA design, in order to:

•            maximise the IA benefit from software implementations

•            reduce the technical challenges

•            ease the evaluation and accreditation burden


Verification framework

The automated verification research group at the Department of Computer Science, Oxford University, was recently awarded a grant from the Engineering and Physical Sciences Research Council (EPSRC) to develop a verification framework for industrial software.

The group has developed machine-assisted methods that can be applied to real-world problems and programming languages, such as control systems for nuclear power stations.

Key strengths include: concurrency, abstraction, industrial-scale hardware verification, software model checking, and verification of real-time and probabilistic systems.

Applications include: security protocols, power management, nanotechnology, and biology.

Verification toolsets include: FDR (model checker), Casper (security protocol compiler), SatAbs (SAT-based model checker for C with predicate abstraction), CBMC (bounded model checker for C) and PRISM (probabilistic model checker) for:

=               Building verifiably correct, robust and reliable state-based, event-driven or concurrent systems.

=               Communicating, reviewing and documenting the behaviour of software components and sub-systems.

=               Ensuring the on going long-term integrity, usability and maintainability of software architecture and design.

Work to implement these methods needs to begin immediately, as they require a sea-change in implementation, validation, evaluation and accreditation. Watch this space for updates as development work continues.

For more information on the issues raised in this INSIGHT, email quoting ‘Verifiable software’.