Visible to the public Biblio

Found 411 results

Filters: Keyword is Analytical models  [Clear All Filters]
2021-01-22
Sahabandu, D., Allen, J., Moothedath, S., Bushnell, L., Lee, W., Poovendran, R..  2020.  Quickest Detection of Advanced Persistent Threats: A Semi-Markov Game Approach. 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS). :9—19.
Advanced Persistent Threats (APTs) are stealthy, sophisticated, long-term, multi-stage attacks that threaten the security of sensitive information. Dynamic Information Flow Tracking (DIFT) has been proposed as a promising mechanism to detect and prevent various cyber attacks in computer systems. DIFT tracks suspicious information flows in the system and generates security analysis when anomalous behavior is detected. The number of information flows in a system is typically large and the amount of resources (such as memory, processing power and storage) required for analyzing different flows at different system locations varies. Hence, efficient use of resources is essential to maintain an acceptable level of system performance when using DIFT. On the other hand, the quickest detection of APTs is crucial as APTs are persistent and the damage caused to the system is more when the attacker spends more time in the system. We address the problem of detecting APTs and model the trade-off between resource efficiency and quickest detection of APTs. We propose a game model that captures the interaction of APT and a DIFT-based defender as a two-player, multi-stage, zero-sum, Stackelberg semi-Markov game. Our game considers the performance parameters such as false-negatives generated by DIFT and the time required for executing various operations in the system. We propose a two-time scale Q-learning algorithm that converges to a Stackelberg equilibrium under infinite horizon, limiting average payoff criteria. We validate our model and algorithm on a real-word attack dataset obtained using Refinable Attack INvestigation (RAIN) framework.
2021-01-20
Focardi, R., Luccio, F. L..  2020.  Automated Analysis of PUF-based Protocols. 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). :304—317.

Physical Unclonable Functions (PUFs) are a promising technology to secure low-cost devices. A PUF is a function whose values depend on the physical characteristics of the underlying hardware: the same PUF implemented on two identical integrated circuits will return different values. Thus, a PUF can be used as a unique fingerprint identifying one specific physical device among (apparently) identical copies that run the same firmware on the same hardware. PUFs, however, are tricky to implement, and a number of attacks have been reported in the literature, often due to wrong assumptions about the provided security guarantees and/or the attacker model. In this paper, we present the first mechanized symbolic model for PUFs that allows for precisely reasoning about their security with respect to a variegate set of attackers. We consider mutual authentication protocols based on different kinds of PUFs and model attackers that are able to access PUF values stored on servers, abuse the PUF APIs, model the PUF behavior and exploit error correction data to reproduce the PUF values. We prove security properties and we formally specify the capabilities required by the attacker to break them. Our analysis points out various subtleties, and allows for a systematic comparison between different PUF-based protocols. The mechanized models are easily extensible and can be automatically checked with the Tamarin prover.

Shi, F., Chen, Z., Cheng, X..  2020.  Behavior Modeling and Individual Recognition of Sonar Transmitter for Secure Communication in UASNs. IEEE Access. 8:2447—2454.

It is necessary to improve the safety of the underwater acoustic sensor networks (UASNs) since it is mostly used in the military industry. Specific emitter identification is the process of identifying different transmitters based on the radio frequency fingerprint extracted from the received signal. The sonar transmitter is a typical low-frequency radiation source and is an important part of the UASNs. Class D power amplifier, a typical nonlinear amplifier, is usually used in sonar transmitters. The inherent nonlinearity of power amplifiers provides fingerprint features that can be distinguished without transmitters for specific emitter recognition. First, the nonlinearity of the sonar transmitter is studied in-depth, and the nonlinearity of the power amplifier is modeled and its nonlinearity characteristics are analyzed. After obtaining the nonlinear model of an amplifier, a similar amplifier in practical application is obtained by changing its model parameters as the research object. The output signals are collected by giving the same input of different models, and, then, the output signals are extracted and classified. In this paper, the memory polynomial model is used to model the amplifier. The power spectrum features of the output signals are extracted as fingerprint features. Then, the dimensionality of the high-dimensional features is reduced. Finally, the classifier is used to recognize the amplifier. The experimental results show that the individual sonar transmitter can be well identified by using the nonlinear characteristics of the signal. By this way, this method can enhance the communication safety of the UASNs.

2021-01-11
Li, Y., Chang, T.-H., Chi, C.-Y..  2020.  Secure Federated Averaging Algorithm with Differential Privacy. 2020 IEEE 30th International Workshop on Machine Learning for Signal Processing (MLSP). :1–6.
Federated learning (FL), as a recent advance of distributed machine learning, is capable of learning a model over the network without directly accessing the client's raw data. Nevertheless, the clients' sensitive information can still be exposed to adversaries via differential attacks on messages exchanged between the parameter server and clients. In this paper, we consider the widely used federating averaging (FedAvg) algorithm and propose to enhance the data privacy by the differential privacy (DP) technique, which obfuscates the exchanged messages by properly adding Gaussian noise. We analytically show that the proposed secure FedAvg algorithm maintains an O(l/T) convergence rate, where T is the total number of stochastic gradient descent (SGD) updates for local model parameters. Moreover, we demonstrate how various algorithm parameters can impact on the algorithm communication efficiency. Experiment results are presented to justify the obtained analytical results on the performance of the proposed algorithm in terms of testing accuracy.
2020-12-28
Makarfi, A. U., Rabie, K. M., Kaiwartya, O., Li, X., Kharel, R..  2020.  Physical Layer Security in Vehicular Networks with Reconfigurable Intelligent Surfaces. 2020 IEEE 91st Vehicular Technology Conference (VTC2020-Spring). :1—6.

This paper studies the physical layer security (PLS) of a vehicular network employing a reconfigurable intelligent surface (RIS). RIS technologies are emerging as an important paradigm for the realisation of smart radio environments, where large numbers of small, low-cost and passive elements, reflect the incident signal with an adjustable phase shift without requiring a dedicated energy source. Inspired by the promising potential of RIS-based transmission, we investigate two vehicular network system models: One with vehicle-to-vehicle communication with the source employing a RIS-based access point, and the other model in the form of a vehicular adhoc network (VANET), with a RIS-based relay deployed on a building. Both models assume the presence of an eavesdropper to investigate the average secrecy capacity of the considered systems. Monte-Carlo simulations are provided throughout to validate the results. The results show that performance of the system in terms of the secrecy capacity is affected by the location of the RIS-relay and the number of RIS cells. The effect of other system parameters such as source power and eavesdropper distances are also studied.

2020-12-17
Rivera, S., Lagraa, S., State, R..  2019.  ROSploit: Cybersecurity Tool for ROS. 2019 Third IEEE International Conference on Robotic Computing (IRC). :415—416.

Robotic Operating System(ROS) security research is currently in a preliminary state, with limited research in tools or models. Considering the trend of digitization of robotic systems, this lack of foundational knowledge increases the potential threat posed by security vulnerabilities in ROS. In this article, we present a new tool to assist further security research in ROS, ROSploit. ROSploit is a modular two-pronged offensive tool covering both reconnaissance and exploitation of ROS systems, designed to assist researchers in testing exploits for ROS.

2020-12-14
Zhou, J.-L., Wang, J.-S., Zhang, Y.-X., Guo, Q.-S., Li, H., Lu, Y.-X..  2020.  Particle Swarm Optimization Algorithm with Variety Inertia Weights to Solve Unequal Area Facility Layout Problem. 2020 Chinese Control And Decision Conference (CCDC). :4240–4245.
The unequal area facility layout problem (UA-FLP) is to place some objects in a specified space according to certain requirements, which is a NP-hard problem in mathematics because of the complexity of its solution, the combination explosion and the complexity of engineering system. Particle swarm optimization (PSO) algorithm is a kind of swarm intelligence algorithm by simulating the predatory behavior of birds. Aiming at the minimization of material handling cost and the maximization of workshop area utilization, the optimization mathematical model of UA-FLPP is established, and it is solved by the particle swarm optimization (PSO) algorithm which simulates the design of birds' predation behavior. The improved PSO algorithm is constructed by using nonlinear inertia weight, dynamic inertia weight and other methods to solve static unequal area facility layout problem. The effectiveness of the proposed method is verified by simulation experiments.
2020-12-11
Ghose, N., Lazos, L., Rozenblit, J., Breiger, R..  2019.  Multimodal Graph Analysis of Cyber Attacks. 2019 Spring Simulation Conference (SpringSim). :1—12.

The limited information on the cyberattacks available in the unclassified regime, hardens standardizing the analysis. We address the problem of modeling and analyzing cyberattacks using a multimodal graph approach. We formulate the stages, actors, and outcomes of cyberattacks as a multimodal graph. Multimodal graph nodes include cyberattack victims, adversaries, autonomous systems, and the observed cyber events. In multimodal graphs, single-modality graphs are interconnected according to their interaction. We apply community and centrality analysis on the graph to obtain in-depth insights into the attack. In community analysis, we cluster those nodes that exhibit “strong” inter-modal ties. We further use centrality to rank the nodes according to their importance. Classifying nodes according to centrality provides the progression of the attack from the attacker to the targeted nodes. We apply our methods to two popular case studies, namely GhostNet and Putter Panda and demonstrate a clear distinction in the attack stages.

Huang, N., Xu, M., Zheng, N., Qiao, T., Choo, K. R..  2019.  Deep Android Malware Classification with API-Based Feature Graph. 2019 18th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/13th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :296—303.

The rapid growth of Android malware apps poses a great security threat to users thus it is very important and urgent to detect Android malware effectively. What's more, the increasing unknown malware and evasion technique also call for novel detection method. In this paper, we focus on API feature and develop a novel method to detect Android malware. First, we propose a novel selection method for API feature related with the malware class. However, such API also has a legitimate use in benign app thus causing FP problem (misclassify benign as malware). Second, we further explore structure relationships between these APIs and map to a matrix interpreted as the hand-refined API-based feature graph. Third, a CNN-based classifier is developed for the API-based feature graph classification. Evaluations of a real-world dataset containing 3,697 malware apps and 3,312 benign apps demonstrate that selected API feature is effective for Android malware classification, just top 20 APIs can achieve high F1 of 94.3% under Random Forest classifier. When the available API features are few, classification performance including FPR indicator can achieve effective improvement effectively by complementing our further work.

2020-12-07
Whitefield, J., Chen, L., Sasse, R., Schneider, S., Treharne, H., Wesemeyer, S..  2019.  A Symbolic Analysis of ECC-Based Direct Anonymous Attestation. 2019 IEEE European Symposium on Security and Privacy (EuroS P). :127–141.
Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.
2020-12-02
Wang, C., Huang, N., Sun, L., Wen, G..  2018.  A Titration Mechanism Based Congestion Model. 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :491—496.

Congestion diffusion resulting from the coupling by resource competing is a kind of typical failure propagation in network systems. The existing models of failure propagation mainly focused on the coupling by direct physical connection between nodes, the most efficiency path, or dependence group, while the coupling by resource competing is ignored. In this paper, a model of network congestion diffusion with resource competing is proposed. With the analysis of the similarities to resource competing in biomolecular network, the model describing the dynamic changing process of biomolecule concentration based on titration mechanism provides reference for our model. Then the innovation on titration mechanism is proposed to describe the dynamic changing process of link load in networks, and a novel congestion model is proposed. By this model, the global congestion can be evaluated. Simulations show that network congestion with resource competing can be obtained from our model.

2020-11-20
Liu, D., Lou, F., Wang, H..  2019.  Modeling and measurement internal threat process based on advanced stochastic model*. 2019 Chinese Automation Congress (CAC). :1077—1081.
Previous research on internal threats was mostly focused on modeling threat behaviors. These studies have paid little attention to risk measurement. This paper analyzed the internal threat scenarios, introduced the operation related protection model into the firewall-password model, constructed a series of sub models. By analyzing the illegal data out process, the analysis model of target network can be rapidly generated based on four protection sub-models. Then the risk value of an assessment point can be computed dynamically according to the Petri net computing characteristics and the effectiveness of overall network protection can be measured. This method improves the granularity of the model and simplifies the complexity of modeling complex networks and can realize dynamic and real-time risk measurement.
2020-11-16
Ibrahim, M., Alsheikh, A..  2018.  Assessing Level of Resilience Using Attack Graphs. 2018 10th International Conference on Electronics, Computers and Artificial Intelligence (ECAI). :1–6.
Cyber-Physical-Systems are subject to cyber-attacks due to existing vulnerabilities in the various components constituting them. System Resiliency is concerned with the extent the system is able to bounce back to a normal state under attacks. In this paper, two communication Networks are analyzed, formally described, and modeled using Architecture Analysis & Design Language (AADL), identifying their architecture, connections, vulnerabilities, resources, possible attack instances as well as their pre-and post-conditions. The generated network models are then verified against a security property using JKind model checker integrated tool. The union of the generated attack sequences/scenarios resulting in overall network compromise (given by its loss of stability) is the Attack graph. The generated Attack graph is visualized graphically using Unity software, and then used to assess the worst Level of Resilience for both networks.
Dwivedi, A..  2018.  Implementing Cyber Resilient Designs through Graph Analytics Assisted Model Based Systems Engineering. 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :607–616.
Model Based Systems Engineering (MBSE) adds efficiency during all phases of the design lifecycle. MBSE tools enforce design policies and rules to capture the design elements, inter-element relationships, and their attributes in a consistent manner. The system elements, and attributes are captured and stored in a centralized MBSE database for future retrieval. Systems that depend on computer networks can be designed using MBSE to meet cybersecurity and resilience requirements. At each step of a structured systems engineering methodology, decisions need to be made regarding the selection of architecture and designs that mitigate cyber risk and enhance cyber resilience. Detailed risk and decision analysis methods involve complex models and computations which are often characterized as a Big Data analytic problem. In this paper, we argue in favor of using graph analytic methods with model based systems engineering to support risk and decision analyses when engineering cyber resilient systems.
2020-10-29
Choi, Seok-Hwan, Shin, Jin-Myeong, Liu, Peng, Choi, Yoon-Ho.  2019.  Robustness Analysis of CNN-based Malware Family Classification Methods Against Various Adversarial Attacks. 2019 IEEE Conference on Communications and Network Security (CNS). :1—6.

As malware family classification methods, image-based classification methods have attracted much attention. Especially, due to the fast classification speed and the high classification accuracy, Convolutional Neural Network (CNN)-based malware family classification methods have been studied. However, previous studies on CNN-based classification methods focused only on improving the classification accuracy of malware families. That is, previous studies did not consider the cases that the accuracy of CNN-based malware classification methods can be decreased under the existence of adversarial attacks. In this paper, we analyze the robustness of various CNN-based malware family classification models under adversarial attacks. While adding imperceptible non-random perturbations to the input image, we measured how the accuracy of the CNN-based malware family classification model can be affected. Also, we showed the influence of three significant visualization parameters(i.e., the size of input image, dimension of input image, and conversion color of a special character)on the accuracy variation under adversarial attacks. From the evaluation results using the Microsoft malware dataset, we showed that even the accuracy over 98% of the CNN-based malware family classification method can be decreased to less than 7%.

2020-10-26
Walker, Aaron, Sengupta, Shamik.  2019.  Insights into Malware Detection via Behavioral Frequency Analysis Using Machine Learning. MILCOM 2019 - 2019 IEEE Military Communications Conference (MILCOM). :1–6.
The most common defenses against malware threats involves the use of signatures derived from instances of known malware. However, the constant evolution of the malware threat landscape necessitates defense against unknown malware, making a signature catalog of known threats insufficient to prevent zero-day vulnerabilities from being exploited. Recent research has applied machine learning approaches to identify malware through artifacts of malicious activity as observed through dynamic behavioral analysis. We have seen that these approaches mimic common malware defenses by simply offering a method of detecting known malware. We contribute a new method of identifying software as malicious or benign through analysis of the frequency of Windows API system function calls. We show that this is a powerful technique for malware detection because it generates learning models which understand the difference between malicious and benign software, rather than producing a malware signature classifier. We contribute a method of systematically comparing machine learning models against different datasets to determine their efficacy in accurately distinguishing the difference between malicious and benign software.
Criswell, John, Zhou, Jie, Gravani, Spyridoula, Hu, Xiaoyu.  2019.  PrivAnalyzer: Measuring the Efficacy of Linux Privilege Use. 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). :593–604.
Operating systems such as Linux break the power of the root user into separate privileges (which Linux calls capabilities) and give processes the ability to enable privileges only when needed and to discard them permanently when the program no longer needs them. However, there is no method of measuring how well the use of such facilities reduces the risk of privilege escalation attacks if the program has a vulnerability. This paper presents PrivAnalyzer, an automated tool that measures how effectively programs use Linux privileges. PrivAnalyzer consists of three components: 1) AutoPriv, an existing LLVM-based C/C++ compiler which uses static analysis to transform a program that uses Linux privileges into a program that safely removes them when no longer needed, 2) ChronoPriv, a new LLVM C/C++ compiler pass that performs dynamic analysis to determine for how long a program retains various privileges, and 3) ROSA, a new bounded model checker that can model the damage a program can do at each program point if an attacker can exploit the program and abuse its privileges. We use PrivAnalyzer to determine how long five privileged open source programs retain the ability to cause serious damage to a system and find that merely transforming a program to drop privileges does not significantly improve security. However, we find that simple refactoring can considerably increase the efficacy of Linux privileges. In two programs that we refactored, we reduced the percentage of execution in which a device file can be read and written from 97% and 88% to 4% and 1%, respectively.
2020-10-19
Dong, Hongbo, Zhu, Qianxiang.  2019.  A Cyber-Physical Interaction Model Based Impact Assessment of Cyberattacks for Internet of Vehicles. 2019 4th International Conference on Communication and Information Systems (ICCIS). :79–83.
Internet of Vehicles are the important part of Intelligence Traffic Systems (ITS), which are essential for the national security and economy development. The impact assessment for cyberattacks in the IoV protection is of great theoretical and practical significance. Most of the researchers in this field pay attention on the attack impact on a vehicle, and the seldom investigate the impact on the whole system which combines all the vehicles as a whole integration. To tackle this problem, a cyber-physical interaction model based impact assessment of cyberattacks is presented. In this approach, the operation of IoV is modeled from the cyberphysical interaction perspective, and then the propagating process from cyber layer to physical layer is investigated. Based on above model, the impact assessment of cyberattacks on IoV is realized quantitatively. Finally, a simulation on an IoV is conducted to verify the effectiveness of this approach.
2020-10-16
Zhang, Rui, Chen, Hongwei.  2019.  Intrusion Detection of Industrial Control System Based on Stacked Auto-Encoder. 2019 Chinese Automation Congress (CAC). :5638—5643.

With the deep integration of industrial control systems and Internet technologies, how to effectively detect whether industrial control systems are threatened by intrusion is a difficult problem in industrial security research. Aiming at the difficulty of high dimensionality and non-linearity of industrial control system network data, the stacked auto-encoder is used to extract the network data features, and the multi-classification support vector machine is used for classification. The research results show that the accuracy of the intrusion detection model reaches 95.8%.

2020-10-12
Okutan, Ahmet, Cheng, Fu-Yuan, Su, Shao-Hsuan, Yang, Shanchieh Jay.  2019.  Dynamic Generation of Empirical Cyberattack Models with Engineered Alert Features. MILCOM 2019 - 2019 IEEE Military Communications Conference (MILCOM). :1–6.
Due to the increased diversity and complexity of cyberattacks, innovative and effective analytics are needed in order to identify critical cyber incidents on a corporate network even if no ground truth data is available. This paper develops an automated system which processes a set of intrusion alerts to create behavior aggregates and then classifies these aggregates into empirical attack models through a dynamic Bayesian approach with innovative feature engineering methods. Each attack model represents a unique collective attack behavior that helps to identify critical activities on the network. Using 2017 National Collegiate Penetration Testing Competition data, it is demonstrated that the developed system is capable of generating and refining unique attack models that make sense to human, without a priori knowledge.
2020-10-06
Akbarzadeh, Aida, Pandey, Pankaj, Katsikas, Sokratis.  2019.  Cyber-Physical Interdependencies in Power Plant Systems: A Review of Cyber Security Risks. 2019 IEEE Conference on Information and Communication Technology. :1—6.

Realizing the importance of the concept of “smart city” and its impact on the quality of life, many infrastructures, such as power plants, began their digital transformation process by leveraging modern computing and advanced communication technologies. Unfortunately, by increasing the number of connections, power plants become more and more vulnerable and also an attractive target for cyber-physical attacks. The analysis of interdependencies among system components reveals interdependent connections, and facilitates the identification of those among them that are in need of special protection. In this paper, we review the recent literature which utilizes graph-based models and network-based models to study these interdependencies. A comprehensive overview, based on the main features of the systems including communication direction, control parameters, research target, scalability, security and safety, is presented. We also assess the computational complexity associated with the approaches presented in the reviewed papers, and we use this metric to assess the scalability of the approaches.

Dattana, Vishal, Gupta, Kishu, Kush, Ashwani.  2019.  A Probability based Model for Big Data Security in Smart City. 2019 4th MEC International Conference on Big Data and Smart City (ICBDSC). :1—6.

Smart technologies at hand have facilitated generation and collection of huge volumes of data, on daily basis. It involves highly sensitive and diverse data like personal, organisational, environment, energy, transport and economic data. Data Analytics provide solution for various issues being faced by smart cities like crisis response, disaster resilience, emergence management, smart traffic management system etc.; it requires distribution of sensitive data among various entities within or outside the smart city,. Sharing of sensitive data creates a need for efficient usage of smart city data to provide smart applications and utility to the end users in a trustworthy and safe mode. This shared sensitive data if get leaked as a consequence can cause damage and severe risk to the city's resources. Fortification of critical data from unofficial disclosure is biggest issue for success of any project. Data Leakage Detection provides a set of tools and technology that can efficiently resolves the concerns related to smart city critical data. The paper, showcase an approach to detect the leakage which is caused intentionally or unintentionally. The model represents allotment of data objects between diverse agents using Bigraph. The objective is to make critical data secure by revealing the guilty agent who caused the data leakage.

2020-10-05
Lago, Loris Dal, Ferrante, Orlando, Passerone, Roberto, Ferrari, Alberto.  2018.  Dependability Assessment of SOA-Based CPS With Contracts and Model-Based Fault Injection. IEEE Transactions on Industrial Informatics. 14:360—369.

Engineering complex distributed systems is challenging. Recent solutions for the development of cyber-physical systems (CPS) in industry tend to rely on architectural designs based on service orientation, where the constituent components are deployed according to their service behavior and are to be understood as loosely coupled and mostly independent. In this paper, we develop a workflow that combines contract-based and CPS model-based specifications with service orientation, and analyze the resulting model using fault injection to assess the dependability of the systems. Compositionality principles based on the contract specification help us to make the analysis practical. The presented techniques are evaluated on two case studies.

Parra, Pablo, Polo, Oscar R., Fernández, Javier, Da Silva, Antonio, Sanchez Prieto, Sebastian, Martinez, Agustin.  2018.  A Platform-Aware Model-Driven Embedded Software Engineering Process Based on Annotated Analysis Models. IEEE Transactions on Emerging Topics in Computing. :1—1.

In this work a platform-aware model-driven engineering process for building component-based embedded software systems using annotated analysis models is described. The process is supported by a framework, called MICOBS, that allows working with different component technologies and integrating different tools that, independently of the component technology, enable the analysis of non-functional properties based on the principles of composability and compositionality. An actor, called Framework Architect, is responsible for this integration. Three other actors take a relevant part in the analysis process. The Component Provider supplies the components, while the Component Tester is in charge of their validation. The latter also feeds MICOBS with the annotated analysis models that characterize the extra-functional properties of the components for the different platforms on which they can be deployed. The Application Architect uses these components to build new systems, performing the trade-off between different alternatives. At this stage, and in order to verify that the final system meets the extra-functional requirements, the Application Architect uses the reports generated by the integrated analysis tools. This process has been used to support the validation and verification of the on-board application software for the Instrument Control Unit of the Energetic Particle Detector of the Solar Orbiter mission.

Rakotonirina, Itsaka, Köpf, Boris.  2019.  On Aggregation of Information in Timing Attacks. 2019 IEEE European Symposium on Security and Privacy (EuroS P). :387—400.

A key question for characterising a system's vulnerability against timing attacks is whether or not it allows an adversary to aggregate information about a secret over multiple timing measurements. Existing approaches for reasoning about this aggregate information rely on strong assumptions about the capabilities of the adversary in terms of measurement and computation, which is why they fall short in modelling, explaining, or synthesising real-world attacks against cryptosystems such as RSA or AES. In this paper we present a novel model for reasoning about information aggregation in timing attacks. The model is based on a novel abstraction of timing measurements that better captures the capabilities of real-world adversaries, and a notion of compositionality of programs that explains attacks by divide-and-conquer. Our model thus lifts important limiting assumptions made in prior work and enables us to give the first uniform explanation of high-profile timing attacks in the language of information-flow analysis.