A crucial component of modern security systems is the task of proving their correctness with respect to a specification, a process known as formal verification.

Future Horizons:

×××

5-yearhorizon

Formal verification becomes more visible

The trend towards demanding explanations for how AI make decisions also drives wider demand for verifiable security and observation of “ceremony” in processes such as key generation. AI accelerates the testing and verification of software and hardware systems, but relatively few companies or organisations have this capacity, creating a threat of monopoly.

10-yearhorizon

Verification methods for biological systems spark debates

Formal verification methods emerge for biological systems, allowing a full analysis of the capability of synthetic organisms before they are made and released into the environment.

25-yearhorizon

Quantum computing introduces new challenges for verification

The challenge of verifying quantum software using quantum techniques drives new research into formal verification based on the laws of physics themselves.

This requires accurate mathematical modelling of hardware designs along with their envisaged operations, and then an exhaustive, systematic check of all model states in a way that can offer evidence of security. While formal verification is an essential part of the development process, in practice it is often applied in retrospect, which makes the task significantly harder. Simpler user interfaces and better techniques could help to change that. This is particularly important for mobile computing and cloud computing, which have spurred the use of formal verification at earlier stages in associated platform development.

Other new types of computing introduce their own challenges for formal verifications. The internet of things, for instance, connects a wide variety of devices together, and to the internet, using a variety of different technologies, communications protocols and security standards, rendering each one vulnerable to attack — especially since they are often installed by non-security experts.¹² 6G communications networks, which are being designed as open and programmable by multiple stakeholders, may be vulnerable to attack in ways that 5G networks are not.¹³

Because of the trend towards ever larger and more complex networks and systems, formal analysis is becoming more difficult, and AI — in particular, its pattern-identification capabilities — will play an increasingly important role in formal verification routines. However, low-end devices are likely to benefit from advances in local verifiability and public verifiability protocols, which will be of particular use in small and medium-sized countries where traditional certification is not affordable, and tools for trustworthy certification (and suitably qualified personnel) are not available.

Formal verification - Anticipation Scores

The Anticipation Potential of a research field is determined by the capacity for impactful action in the present, considering possible future transformative breakthroughs in a field over a 25-year outlook. A field with a high Anticipation Potential, therefore, combines the potential range of future transformative possibilities engendered by a research area with a wide field of opportunities for action in the present. We asked researchers in the field to anticipate:

The uncertainty related to future science breakthroughs in the field
The transformative effect anticipated breakthroughs may have on research and society
The scope for action in the present in relation to anticipated breakthroughs.

This chart represents a summary of their responses to each of these elements, which when combined, provide the Anticipation Potential for the topic. See methodology for more information.