Using the power of Dezyne’s verification and validation features to build cyber resilient applications

Using the power of Dezyne’s verification and validation features to build cyber resilient applications
How resilient is your application?

Imagine for a moment that an intruder has gained access to your network. There are various ways in which they might seek to compromise your operations. One of the simplest, blunt force methods is to look for an application with network interfaces and attempt to disrupt it by firing events at random into its exposed APIs. A more sophisticated attack could seek to influence the behaviour of an application by observing the flow of events and responses at an exposed API and attempting to unravel the semantics of the application’s interface. In either case the application will be exposed to unexpected, potentially errant behaviour. How certain are you that your software systems are resilient enough to cope with such an attack? How can you build cyber resilient applications?

What’s the problem?

Simply put, software systems are mind-bogglingly complex, to the extent that no human can begin to comprehend the entirety of their possible behaviour. One of the main causes of complexity is the often-unavoidable introduction of asynchronicity and concurrency into software designs and the consequential explosion of the number of ways in which a design can behave, its “state space”. Unfortunately, asynchronicity is frequently accompanied by its ugly sibling, non-determinism, which effectively prevents the majority of an application’s state space being tested by conventional testing tools and methods. It is this gap in our understanding that an attacker seeks to exploit: push an application into untested state space by firing unexpected or errant behaviour into it and it’s very likely to collapse in a quivering heap.

How Dezyne helps with verification and validation

Imagine instead that the behaviour of a software system could be confined to a fully understood and tested set of pathways, that in effect it became a cyclic automaton constrained to repeating only known behaviour and nothing else. Such a system would then become impervious to attacks based on the injection of unexpected or errant behaviour, consequently displaying a high degree of resiliency. Additionally, the system could be instrumented to detect unexpected behaviour and react accordingly, adding further to its resiliency. This is what Dezyne enables you to accomplish.

Dezyne provides engineers with the ability to specify and design the behaviour of software components in terms of models. These models are automatically, formally verified for completeness and a range of behavioural correctness properties including illegal behaviour, race conditions and deadlocks, amongst others. Completeness means that the relationship between the events that a model accepts and the responses that it provides is a closed set, with no missing behaviour or forgotten edge conditions.

Verifying correctness

Verification of correctness involves the mathematical expansion of the entire state space of a set of models and the application of theorems to every path through the space. The result is the knowledge that, for the properties that were verified, the behaviour of the models is fully understood.

Further, Dezyne can be used in combination with an “armour” design pattern [reference to my Software Archaeology paper] to detect illegal or errant behaviour on external or exposed interfaces. Should a client attempt to act outside of the protocol defined by an armoured interface, the armouring layer will detect the violation and can be designed to take appropriate actions, increasing the resiliency of your application even further.

Ultimately, through the application of automated formal methods, Dezyne demonstrates that a software design behaves as a cyclic automaton, constrained to executing only known behaviour and results in applications with a high degree of cyber resiliency.