the foundation
of our solutions
the foundation
of our solutions
Runtime Verification Techniques as a Comprehensive Stream Processing Toolset
Processing data in real-time – also known as stream processing – is a central requirement in a multitude of applications: from observation of natural phenomena (eg, telescope observations [1]), to security enforcement (eg, video processing [1], mobile device policy checking [2,3], financial transaction monitoring [4,5], secure communication protocols [6,7] and smart contracts [8]), to streams of data generated through online user interactions (eg, user experience enhancement [1], social media interactions to protect privacy [9] or extract business intelligence [10]).
As a basic requirement, these applications usually require aggressive optimisation so that the time window available for processing suffices, and massively scalable technology ensuring that large volumes of data can be handled. More advanced systems typically also allow domain experts to customise processes as required by the continuously changing environment, and enable them to directly trigger actions and compensations in response to the observations.
An area which shares the same concerns of event observation and processing in a highly efficient manner, is runtime verification (¹also referred to as runtime monitoring). While this field of research was initially thought of as a way of non-intrusively detecting bugs of an executing software, the developed techniques are also more generally applicable to stream processing. This connection, as well as the advantages of runtime verification in terms of structure and modularity, gave rise to monitor-oriented programming, i.e., a way of reasoning about pattern matching algorithms and software organisation in terms of monitors.
Optimisation
Real-time monitoring requires strict management of the available time window to process the incoming data and take any necessary action. As a prerequisite, this requires:
Efficient organisation and storage of data
For quick access, data and intermediate results are stored in an easily searchable manner. This enables fast access to the history without needing to perform complex and expensive queries. Setting up a dataset with optimised data might be a significant initial cost, for example if lots of historical non-optimised data is available. Therefore, it is useful at times to have dedicated processes which are able to jumpstart the optimisation process for quick and seamless initialisation [11].
Splitting processing into what needs to be done now and what can wait
In various applications, such as user interaction, the volume of incoming data is non-uniform; meaning that spikes of activity are encountered at particular intervals. To make sure that no data is lost, or crucial alerts missed, the processing of such data is organised into that which is urgent and that which can possibly wait (perhaps a few seconds) [5]. In such scenarios, monitoring may support various levels of priority by supporting different levels of synchronicity – from fully synchronous monitoring (eg, a transaction does not proceed before monitor clearance), to fully asynchronous (eg, compiling end of year statistics by processing database records).
Robustness
Dealing with a high volume of incoming data and tight reaction timeframes, necessitates robust components such as efficient buffering, data structures such as indices for efficient data lookup, load balancing mechanisms, redundant components in case of failure, etc. All these parts contribute to the required robustness, ensuring consistent and reliable performance. A preferred way of organising the processing components is through microservices – providing a way of splitting each monitoring task into a highly specialised service [12]. These services are easily replicable and failure can quickly be localised.
Domain Customisation
One of the biggest hurdles to successful data processing is the need of highly specialised and dynamic domain knowledge to be taken into consideration. The constant communication required between the technical software developers and the non-technical domain experts can severely hamper quick and smooth deployment of systems and updates. One way of circumventing this issue is to provide a domain-specific language which bridges the gap, enabling domain experts to directly configure the data processing engine. This approach can enable a business analyst to specify – using a controlled natural language – when to be alerted by a competitor’s action [9], a fraud expert to express directly which tax returns should be flagged [12], or an AML expert to specify compliance rules [14].
Actions And Compensations
In many cases, a dashboard is the end result of the data processing journey, however in several scenarios it is desirable for the system to go beyond the dashboard and take automated action in response. The range of possible actions can include sending an email or SMS to a human operator, or more proactively taking decisions on behalf of humans.
Interestingly, in areas such as pattern recognition, a pattern might be detected when some damage has already been done. This is where the concept of a ‘compensation’ might come in handy, providing a way of undoing – to varying degrees – the undesirable consequences of the past. In the context of financial transactions, this might mean reversing those transactions which have not yet been committed, or performing a transaction which cancels the previous offending one [5,15,16,17].
Future Directions
We have a clear path for the research in the short and medium term, although we remain open in terms of enhancing our technology with other areas of study. We are currently studying in more depth the integration of both simple and more complex AI algorithms at different stages and levels in the monitoring process.
AI will be used to automatically prioritise and group alerts. When incoming data volumes are high, alerts may start flooding in without a clear connection between them. Typically, these would be related to single problem (e.g., a bonus release in a gaming scenario). Having the support of AI to find the connections across several alerts would greatly simplify the task of the human operator or decision maker, to make sense of the situation and remedy it in minimal time.
Another area which offers lots of promise is the area of anomaly detection. The vast majority of deployed AI algorithms aim to detect known patterns of behaviour (e.g., a pattern of fraud which has been detected). This is useful, but does not protect against yet unseen patterns which fraudsters attempt to devise on a continuous game of cat and mouse. Thus, combining anomaly detection with runtime monitoring is one of our next goals.
Runtime Verification Techniques as a Comprehensive Stream Processing Toolset
Processing data in real-time – also known as stream processing – is a central requirement in a multitude of applications: from observation of natural phenomena (eg, telescope observations [1]), to security enforcement (eg, video processing [1], mobile device policy checking [2,3], financial transaction monitoring [4,5], secure communication protocols [6,7] and smart contracts [8]), to streams of data generated through online user interactions (eg, user experience enhancement [1], social media interactions to protect privacy [9] or extract business intelligence [10]).
As a basic requirement, these applications usually require aggressive optimisation so that the time window available for processing suffices, and massively scalable technology ensuring that large volumes of data can be handled. More advanced systems typically also allow domain experts to customise processes as required by the continuously changing environment, and enable them to directly trigger actions and compensations in response to the observations.
An area which shares the same concerns of event observation and processing in a highly efficient manner, is runtime verification (¹also referred to as runtime monitoring). While this field of research was initially thought of as a way of non-intrusively detecting bugs of an executing software, the developed techniques are also more generally applicable to stream processing. This connection, as well as the advantages of runtime verification in terms of structure and modularity, gave rise to monitor-oriented programming, i.e., a way of reasoning about pattern matching algorithms and software organisation in terms of monitors.
Optimisation
Real-time monitoring requires strict management of the available time window to process the incoming data and take any necessary action. As a prerequisite, this requires:
Efficient organisation and storage of data
For quick access, data and intermediate results are stored in an easily searchable manner. This enables fast access to the history without needing to perform complex and expensive queries. Setting up a dataset with optimised data might be a significant initial cost, for example if lots of historical non-optimised data is available. Therefore, it is useful at times to have dedicated processes which are able to jumpstart the optimisation process for quick and seamless initialisation [11].
Splitting processing into what needs to be done now and what can wait
In various applications, such as user interaction, the volume of incoming data is non-uniform; meaning that spikes of activity are encountered at particular intervals. To make sure that no data is lost, or crucial alerts missed, the processing of such data is organised into that which is urgent and that which can possibly wait (perhaps a few seconds) [5]. In such scenarios, monitoring may support various levels of priority by supporting different levels of synchronicity – from fully synchronous monitoring (eg, a transaction does not proceed before monitor clearance), to fully asynchronous (eg, compiling end of year statistics by processing database records).
Robustness
Dealing with a high volume of incoming data and tight reaction timeframes, necessitates robust components such as efficient buffering, data structures such as indices for efficient data lookup, load balancing mechanisms, redundant components in case of failure, etc. All these parts contribute to the required robustness, ensuring consistent and reliable performance. A preferred way of organising the processing components is through microservices – providing a way of splitting each monitoring task into a highly specialised service [12]. These services are easily replicable and failure can quickly be localised.
Domain Customisation
One of the biggest hurdles to successful data processing is the need of highly specialised and dynamic domain knowledge to be taken into consideration. The constant communication required between the technical software developers and the non-technical domain experts can severely hamper quick and smooth deployment of systems and updates. One way of circumventing this issue is to provide a domain-specific language which bridges the gap, enabling domain experts to directly configure the data processing engine. This approach can enable a business analyst to specify – using a controlled natural language – when to be alerted by a competitor’s action [9], a fraud expert to express directly which tax returns should be flagged [12], or an AML expert to specify compliance rules [14].
Actions And Compensations
In many cases, a dashboard is the end result of the data processing journey, however in several scenarios it is desirable for the system to go beyond the dashboard and take automated action in response. The range of possible actions can include sending an email or SMS to a human operator, or more proactively taking decisions on behalf of humans.
Interestingly, in areas such as pattern recognition, a pattern might be detected when some damage has already been done. This is where the concept of a ‘compensation’ might come in handy, providing a way of undoing – to varying degrees – the undesirable consequences of the past. In the context of financial transactions, this might mean reversing those transactions which have not yet been committed, or performing a transaction which cancels the previous offending one [5,15,16,17].
Future Directions
We have a clear path for the research in the short and medium term, although we remain open in terms of enhancing our technology with other areas of study. We are currently studying in more depth the integration of both simple and more complex AI algorithms at different stages and levels in the monitoring process.
AI will be used to automatically prioritise and group alerts. When incoming data volumes are high, alerts may start flooding in without a clear connection between them. Typically, these would be related to single problem (e.g., a bonus release in a gaming scenario). Having the support of AI to find the connections across several alerts would greatly simplify the task of the human operator or decision maker, to make sense of the situation and remedy it in minimal time.
Another area which offers lots of promise is the area of anomaly detection. The vast majority of deployed AI algorithms aim to detect known patterns of behaviour (e.g., a pattern of fraud which has been detected). This is useful, but does not protect against yet unseen patterns which fraudsters attempt to devise on a continuous game of cat and mouse. Thus, combining anomaly detection with runtime monitoring is one of our next goals.
References & Other Studies
Runtime Verification for Stream Processing Applications
Christian Colombo, Gordon Pace, Luke Camilleri, Claire Dimech, Reuben Farrugia, Jean Paul Grech, Alessio Magro, Andrew C Sammut, Kristian Zarb Adami, ISoLA, Corfu, Greece, 2016.
Runtime verification (RV) has long been applied beyond its strict delineation of verification, through the notion of monitor-oriented programming. In this paper we present a portfolio of real-life case studies where RV is used to program stream-processing systems directly — where all the logic of the implemented system is defined in terms of monitors. The systems include the processing of Facebook events for business intelligence, analysing users’ activity log for detecting UI usability issues, video frame analysis for human movement detection, and telescope signals processing for pulsar identification.
Device-Centric Monitoring for Mobile Device Management
Luke Chircop, Christian Colombo and Gordon Pace, FESCA, Eindhoven, The Netherlands, 2016
The ubiquity of computing devices has led to an increased need to ensure not only that the applications deployed on them are correct with respect to their specifications, but also that the devices are used in an appropriate manner, especially in situations where the device is provided by a party other than the actual user. Much work which has been done on runtime verification for mobile devices and operating systems is mostly application-centric, resulting in global, device-centric properties (e.g. the user may not send more than 100 messages per day across all applications) being difficult or impossible to verify. In this paper we present a device-centric approach to runtime verify the device behaviour against a device policy with the different applications acting as independent components contributing to the overall behaviour of the device. We also present an implementation for Android devices, and evaluate it on a number of device-centric policies, reporting the empirical results obtained.
BYOD for Android - Just add Java
Jessica Buttigieg, Mark Vella and Christian Colombo, TRUST, Crete, Greece, 2015
Bring-Your-Own-Device (BYOD) implies that the same mobile device is used for both work and personal purposes. This poses a security concern where untrusted userinstalled applications might interfere maliciously with corporate ones. Android’s existing fixed permissions mechanism is not a suitable countermeasure. Malware isolation through virtualization1 and managed device scans2 is possible, however a complete solution requires a context-specific (work/personal) policy mechanism. Our proposition, BYOD-RV, uses Dynamic Binary Instrumentation (DBI) and Runtime Verification (RV). DBI (in-memory code patching) avoids Android source code changes as typically required by similar approaches.
Dynamic Event-Based
Runtime Monitoring of Real-Time and Contextual Properties
Christian Colombo, Gordon J. Pace and Gerardo Schneider, in FMICS 2008, Italy
Given the intractability of exhaustively verifying software, the use of runtime-verification, to verify single execution paths at runtime, is becoming popular. Although the use of runtime verification is increasing in industrial settings, various challenges still are to be faced to enable it to spread further. We present dynamic communicating automata with timers and events to describe properties of systems, implemented in Larva, an event-based runtime verification tool for monitoring temporal and contextual properties of Java programs. The combination of timers with dynamic automata enables the straightforward expression of various properties, including replication of properties, as illustrated in the use of Larva for the runtime monitoring of a real life case study — an online transaction system for credit card. The features of Larva are also benchmarked and compared to a number of other runtime verification tools, to assess their respective strengths in property expressivity and overheads induced through monitoring.
Safer Asynchronous
Runtime Monitoring Using Compensations
Christian Colombo,
Gordon Pace and Patrick Abela, in Formal Methods in System Design, 41(3):
269-294, 2012
Asynchronous monitoring relieves the system from additional overheads induced through online runtime monitoring. The price paid with such monitoring approaches is that the system may proceed further despite having reached an anomalous state. Any actions performed by the system after the error occurring are undesirable, since for instance, an unchecked malicious user access may perform unauthorized actions. In this paper we investigate the use of compensations to enable the undoing of such undesired actions, thus enriching asynchronous monitoring with the ability to restore the system to the original state just after the anomaly had occurred. Furthermore, we show how adaptive synchronisation and desynchronisation of the monitor with the system can also be achieved and report on the use of the proposed approach on an industrial case study of a financial transaction handling system.
Towards a Comprehensive
Solution for Secure Cryptographic Protocol Execution based on Runtime
Verification
Christian Colombo and Mark Vella, in ForSE, Valletta, Malta, 2020
Analytical security of cryptographic protocols does not immediately translate to operational security due to incorrect implementation and attacks targeting the execution environment. Code verification and hardware based trusted execution solutions exist, however these leave it up to the implementer to assemble the complete solution, and imposing a complete re-think of the hardware platforms and software development process. We rather aim for a comprehensive solution for secure cryptographic protocol execution, based on runtime verification and stock hardware security modules that can be deployed on existing platforms and protocol implementations. A study using a popular web browser shows promising results with respect to practicality.
Secure Communication in the Quantum Era: (Group) Key Establishment
Christian Colombo,
María Isabel González Vasco, Rainer Steinwandt, and Pavol Zajac, in Advanced
Technologies for Security Applications, NATO Science for Peace and Security,
2020.
Technology has been the spark that ignited NATO’s interest and commitment to scientific advancement during its history. Since its creation, the Science for Peace and Security (SPS) Programme has been instrumental to NATO’s commitment to innovation, science and technological advancement. During the years, SPS has demonstrated a flexible and versatile approach to practical scientific cooperation, and has promoted knowledge-sharing, building capacity, and projected stability outside NATO territory. The priorities addressed by the SPS Programme are aligned with NATO’s strategic objectives, and aim to tackle emerging security challenges that require dynamic adaptation for the prevention and mitigation of risks. By addressing priorities such as advanced technologies, hybrid threats, and counter-terrorism, the Programme deals with new, contemporary challenges. On 17-18 September 2019, the SPS Programme gathered at the KU Leuven University a wide number of researchers from a selection of on-going and recently closed SPS projects in the field of security-related advanced technologies for a “Cluster Workshop on Advanced Technologies”. The workshop covered, in particular, the following scientific domains: communication systems, advanced materials, sensors and detectors, and unmanned and autonomous systems. This book provides an overview on how these projects have contributed to the development of new technologies and innovative solutions and recommendations for future actions in the NATO SPS programme.
Contracts over Smart Contracts: Recovering from Violations Dynamically
Christian Colombo, Joshua Ellul, and Gordon Pace, in ISoLA, Limassol, Cyprus, 2018
Smart contracts which enforce behaviour between parties have been hailed as a new way of regulating business, particularly on public distributed ledger technologies which ensure the immutability of smart contracts, and can do away with points of trust. Many such platforms, including Ethereum, come with a virtual machine on which smart contracts are executed, described in an imperative manner. Given the critical nature of typical smart contract applications, their bugs and vulnerabilities have proved to be particularly costly. In this paper we argue how dynamic analysis can be used not only to identify errors in the contracts, but also to support recovery from such errors. Furthermore, contract immutability means that code cannot be easily fixed upon discovering a problem. To address this issue, we also present a specification-driven approach, allowing developers to promise behavioural properties via smart contracts, but still allowing them to update the code which implements the specification in a safe manner.
An Automata-Based Approach to Evolving Privacy Policies for Social Networks
Raúl Pardo, Christian Colombo, Gordon J. Pace, Gerardo Schneider, RV, Madrid, Spain, 2016
Online Social Networks (OSNs) are ubiquitous, with more than 70% of Internet users being active users of such networking services. This widespread use of OSNs brings with it big threats and challenges, privacy being one of them. Most OSNs today offer a limited set of (static) privacy settings and do not allow for the definition, even less enforcement, of more dynamic privacy policies. In this paper we are concerned with the specification and enforcement of dynamic (and recurrent) privacy policies that are activated or deactivated by context (events). In particular, we present a novel formalism of policy automata, transition systems where privacy policies may be defined per state. We further propose an approach based on runtime verification techniques to define and enforce such policies. We provide a proof-of-concept implementation for the distributed social network Diaspora, using the runtime verification tool LARVA to synthesise enforcement monitors.
A Controlled Natural Language for Business Intelligence Monitoring
Christian Colombo, Jean Paul Grech, and Gordon Pace, NLDB, Passau, Germany, 2015
With ever increasing information available in social networks, the number of businesses attempting to exploit it is on the rise, particularly by keeping track of their customers’ posts and likes on social media sites like Facebook. Whilst APIs can be used to automate the tracking
process, writing scripts to extract information and process it requires considerable technical skill and is thus not an option for non technical business analysts. On the other hand, off-the-shelf business intelligence solutions do not provide the desired flexibility for the specific needs of particular businesses. In this paper, we present a controlled natural language enabling non-technical users to express their queries in a language they can easily understand but which can be directly compiled into executable code.
Fast-Forward Runtime Monitoring - An Industrial Case Study
Christian Colombo, and Gordon Pace, RV, Istanbul, Turkey, 2012
Amongst the challenges of statefully monitoring large-scale industrial systems is the ability to efficiently advance the monitors to the current state of the system. This problem presents itself under various guises such as when a monitoring system is being deployed for the first time, when monitors are changed and redeployed, and when asynchronous monitors fall too much behind the system. We propose fast-forward monitoring — a means of reaching the monitoring state at a particular point in time in an efficient manner, without actually traversing all the transitions leading to that state, and which we applied to a financial transaction system with millions of transactions already affected. In this paper we discuss our experience and present a generic theory of monitor fast-forwarding instantiating it for efficient monitor deployment in real-life systems.
Runtime Verification using Valour
Shaun Azzopardi, Christian Colombo, Jean Paul Ebejer, Edward Mallia, and Gordon Pace, RV-CuBES, Seattle, USA, 2017
In this paper we give an overview of Valour, a runtime verification tool which has been developed in the context of a project to act as a backend verification tool for financial transaction software. A Valour script is written by the user and is then compiled into a verification system. Although, developed as part of a project, the tool has been designed as a stand-alone general-purpose verification engine with a particular emphasis on event consumption. The strong points of Valour when compared to other runtime verification tools is its focus on scalability and robustness.
A Controlled Natural Language For Tax Fraud Detection
Aaron Calafato, Christian Colombo, Gordon Pace and Brian Vella, CNL, Aberdeen, UK, 2016
Addressing tax fraud has been taken increasingly seriously, but most attempts to uncover it involve the use of human fraud experts to identify and audit suspicious cases. To identify such cases, they come up with patterns which an IT team then implements to extract matching instances. The process, starting from the communication of the patterns to the developers, the debugging of the implemented code, and the refining of the rules, results in a lengthy and errorprone iterative methodology. In this paper, we present a framework where the fraud expert is empowered to independently design tax fraud patterns through a controlled natural language implemented in GF, enabling immediate feedback reported back to the fraud expert. This allows multiple refinements of the rules until optimised, all within a timely manner. The approach has been evaluated by a number of fraud experts working with the Maltese Inland Revenue Department.
A Controlled Natural Language for Financial Services Compliance Checking
Shaun Azzopardi, Christian Colombo and Gordon Pace, in CNL, Co Kildare, Ireland, 2018
Controlled natural languages have long been used as a surface form for formal descriptions, allowing easy transitioning between natural language specifications and implementable specifications. In this paper we motivate the use of a controlled natural language in the representation and verification of financial services regulations. The verification context is that of payment applications that come with a model of their promised behaviour and which are deployed on a payments ecosystem. The semantics of this financial services regulations controlled natural language (FSRCNL) can produce compliance checks that analyse both the promised model and/or monitor the application itself after it is deployed.
Compensation-Aware Runtime Monitoring
Christian Colombo, Gordon J. Pace and Patrick Abela, in RV, Malta, 2010
To avoid large overheads induced by runtime monitoring, the use of asynchronous log-based monitoring is sometimes adopted — even though this implies that the system may proceed further despite having reached an anomalous state. Any actions performed by the system after the error occurring are undesirable, since for instance, an unchecked malicious user may perform unauthorized actions. Since stopping such actions is not feasible, in this paper we investigate the use of compensations to enable the undoing of actions, thus enriching asynchronous monitoring with the ability to restore the system to the original state in which the anomaly occurred. Furthermore, we show how allowing the monitor to adaptively synchronise and desynchronise with the system is also possible and report on the use of the approach on an industrial case study of a financial transaction system.
Monitor-Oriented Compensation Programming Through Compensating Automata
Christian Colombo and Gordon Pace, ECEASST 58, 2013
Compensations have been used for decades in areas such as flow management systems, long-lived transactions and more recently in the service oriented architecture. Since compensations enable the logical reversal of past actions, by their nature they crosscut other programming concerns. Thus, intertwining compensations with the rest of the system not only makes programs less well structured, but also limits the expressivity of compensations due to the tight coupling with the system’s behaviour. To separate compensation concerns from the normal system behaviour, we propose compensating automata, a graphical specification language dedicated to compensation programming. Compensating automata are subsequently employed in a monitor-oriented fashion to program compensations without cluttering the actual system implementation. This approach is shown applicable to a complex case study which existing compensation approaches have difficulty handling.
Comprehensive Monitor-Oriented Compensation Programming
Christian Colombo and Gordon Pace, FESCA, Grenoble, France, 2014
Compensation programming is typically used in the programming of web service compositions whose correct implementation is crucial due to their handling of security-critical activities such as financial transactions. While traditional exception handling depends on the state of the system at the moment of failure, compensation programming is significantly more challenging and dynamic because it is dependent on the runtime execution flow — with the history of behaviour of the system at the moment of failure affecting how to apply compensation. To address this dynamic element, we propose the use of runtime monitors to facilitate compensation programming, with monitors enabling the modeller to be able to implicitly reason in terms of the runtime control flow, thus separating the concerns of system building and compensation modelling. Our approach is instantiated into an architecture and shown to be applicable to a case study.