Biblio

In Cloud Computing, a wide range of virtual platforms are integrated and offer users a flexible pay-as-you-need service. Compared to conventional computing systems, the provision of an acceptable degree of resilience to cloud services is a daunting challenge due to the complexities of the cloud environment and the need for efficient technology that could sustain cloud advantages over other technologies. For a cloud guest resilience service solution, we provide architectural design, installation specifics, and performance outcomes throughout this article. Virtual Machine Manager (VMM) enables execution statistical test of the virtual machine states to be monitored and avoids to reach faulty states.

Traditional passive defense methods cannot resist the constantly updated and evolving cyber attacks. The concept of resilience is introducing to measure the ability of the system to maintain its function under attack. It matters in evaluating the security of modern industrial systems. This paper presents a 3D Resilience State Space method to assess Communication-based train control (CBTC) system resilience under malware attack. We model the spread of malware as two functions: the communicability function \$f\$(x) and the susceptibility function 9 (x). We describe the characteristics of these two function in the CBTC complex network by using the percolation theory. Then we use a perturbation formalism to analyze the impact of malware attack on information flow and use it as an indicator of the cyber layer state. The CBTC cyber-physical system resilience metric formalizes as the system state transitions in three-dimensional state space. The three dimensions respectively represent the cyber layer state, the physical layer state, and the transmission layer state. The simulation results reveal that the proposed framework can effectively assess the resilience of the CBTC system. And the anti-malware programs can prevent the spread of malware and improve CBTC system resilience.

The load margin due to voltage instability and small-signal instability can be a valuable measure for the operator of the power system to ensure a continuous and safe supply of electricity. However, if this load margin was calculated without considering system operating requirements, then this margin may not be adequate. This article proposes an algorithm capable of providing the power system load margin considering the requirements of voltage stability, small-signal stability, and operational requirements, as limits of reactive power generation of synchronous generators in dynamic security assessment. Case studies were conducted in the 107-bus reduced order Brazilian system considering a list of contingencies and directions of load growth.

Continuous Integration (CI) and Continuous Delivery (CD) have become a well-known practice in DevOps to ensure fast delivery of new features. This is achieved by automatically testing and releasing new software versions, e.g. multiple times per day. However, classical security management techniques cannot keep up with this quick Software Development Life Cycle (SDLC). Nonetheless, guaranteeing high security quality of software systems has become increasingly important. The new trend of DevSecOps aims to integrate security techniques into existing DevOps practices. Especially, the automation of security testing is an important area of research in this trend. Although plenty of literature discusses security testing and CI/CD practices, only a few deal with both topics together. Additionally, most of the existing works cover only static code analysis and neglect dynamic testing methods. In this paper, we present an approach to integrate three automated dynamic testing techniques into a CI/CD pipeline and provide an empirical analysis of the introduced overhead. We then go on to identify unique research/technology challenges the DevSecOps communities will face and propose preliminary solutions to these challenges. Our findings will enable informed decisions when employing DevSecOps practices in agile enterprise applications engineering processes and enterprise security.

Existing security models are highly linear and fail to capture the rich interactions that occur across security technology, infrastructure, cybersecurity, and human/organizational components. In this work, we will leverage insights from resilience science, complex system theory, and network theory to develop a next-generation security model based on these interactions to address challenges in complex, nonlinear risk environments and against innovative and disruptive technologies. Developing such a model is a key step forward toward a dynamic security paradigm (e.g., shifting from detection to anticipation) and establishing the foundation for designing next-generation physical security systems against evolving threats in uncontrolled or contested operational environments.

Incast traffic is a many-to-one communication pattern used in many applications, including distributed storage, web-search with partition/aggregation design pattern, and MapReduce, commonly in data centers. It is generally composed of short-lived flows that may be queued behind large flows' packets in congested switches where performance degradation is observed. Smart buffering at the switch level is sensed to mitigate this issue by automatically and dynamically adapting to traffic conditions changes in the highly dynamic data center environment. But for this dynamic and smart buffer management to become effectively beneficial for all the traffic, and especially for incast the most critical one, incast performance models that provide insights on how various factors affect it are needed. The literature lacks these types of models. The existing ones are analytical models, which are either tightly coupled with a particular protocol version or specific to certain empirical data. Motivated by this observation, we propose a machine-learning-based incast performance inference. With this prediction capability, smart buffering scheme or other QoS optimization algorithms could anticipate and efficiently optimize system parameters adjustment to achieve optimal performance. Since applying machine learning to networks managed in a distributed fashion is hard, the prediction mechanism will be deployed on an SDN control plane. We could then take advantage of SDN's centralized global view, its telemetry capabilities, and its management flexibility.

The secure functioning of automotive systems is vital to the safety of their passengers and other roadway users. One of the critical functions for safety is the controller area network (CAN), which interconnects the safety-critical electronic control units (ECUs) in the majority of ground vehicles. Unfortunately CAN is known to be vulnerable to several attacks. One such attack is the bus-off attack, which can be used to cause a victim ECU to disconnect itself from the CAN bus and, subsequently, for an attacker to masquerade as that ECU. A limitation of the bus-off attack is that it requires the attacker to achieve tight synchronization between the transmission of the victim and the attacker's injected message. In this paper, we introduce a schedule-based attack framework for the CAN bus-off attack that uses the real-time schedule of the CAN bus to predict more attack opportunities than previously known. We describe a ranking method for an attacker to select and optimize its attack injections with respect to criteria such as attack success rate, bus perturbation, or attack latency. The results show that vulnerabilities of the CAN bus can be enhanced by schedule-based attacks.

In this paper, we highlight a fundamental vulnerability associated with the widely adopted “Just Tap” push-based authentication in the face of a concurrency attack, and propose the method REPLICATE, a redesign to counter this vulnerability. In the concurrency attack, the attacker launches the login session at the same time the user initiates a session, and the user may be fooled, with high likelihood, into accepting the push notification which corresponds to the attacker's session, thinking it is their own. The attack stems from the fact that the login notification is not explicitly mapped to the login session running on the browser in the Just Tap approach. REPLICATE attempts to address this fundamental flaw by having the user approve the login attempt by replicating the information presented on the browser session over to the login notification, such as by moving a key in a particular direction, choosing a particular shape, etc. We report on the design and a systematic usability study of REPLICATE. Even without being aware of the vulnerability, in general, participants placed multiple variants of REPLICATE in competition to the Just Tap and fairly above PIN-based authentication.

Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challenging programs, but they typically require significant human assistance, and cannot handle modules or higher-order programs.To connect these two approaches, we present SeLoC—a separation logic for non-interference, on top of which we build a type system using the technique of logical relations. By building a type system on top of separation logic, we can compositionally verify programs that consist of typed and untyped parts. The former parts are verified through type checking, while the latter parts are verified through manual proof.The core technical contribution of SeLoC is a relational form of weakest preconditions that can track information flow using separation logic resources. SeLoC is fully machine-checked, and built on top of the Iris framework for concurrent separation logic in Coq. The integration with Iris provides seamless support for fine-grained concurrency, which was beyond the reach of prior type systems and program logics for non-interference.

The fifth-generation (5G) standard is the last telecommunication technology, widely considered to have the most important characteristics in the future network industry. The 5G system infrastructure contains three principle interfaces, each one follows a set of protocols defined by the 3rd Generation Partnership Project group (3GPP). For the next generation network, 3GPP specified two authentication methods systematized in two protocols namely 5G Authentication and Key Agreement (5G-AKA) and Extensible Authentication Protocol (EAP). Such protocols are provided to ensure the authentication between system entities. These two protocols are critical systems, thus their reliability and correctness must be guaranteed. In this paper, we aim to formally re-examine 5G-AKA protocol using micro Common Representation Language 2 (mCRL2) language to verify such a security protocol. The mCRL2 language and its associated toolset are formal tools used for modeling, validation, and verification of concurrent systems and protocols. In this context, the authentication protocol 5G-AKA model is built using Algebra of Communication Processes (ACP), its properties are specified using Modal mu-Calculus and the properties analysis exploits Model-Checker provided with mCRL2. Indeed, we propose a new mCRL2 model of 3GPP specification considering 5G-AKA protocol and we specify some properties that describe necessary requirements to evaluate the correctness of the protocol where the parsed properties of Deadlock Freedom, Reachability, Liveness and Safety are positively assessed.

Compared with other virtualization technologies, container technology is widely used in edge computing because of its low cost, high reliability, high flexibility and fast portability. However, the use of container technology can alleviate the pressure of massive data, but also bring complex and diverse security problems. Reliable information security risk assessment method is the key to ensure the smooth application of container technology. According to the risk assessment theory, a security risk assessment method for edge computing containers based on dynamic game theory is proposed. Aiming at the complex container security attack and defense process, the container system's security model is constructed based on dynamic game theory. By combining the attack and defense matrix, the Nash equilibrium solution of the model is calculated, and the dynamic process of the mutual game between security defense and malicious attackers is analyzed. By solving the feedback Nash equilibrium solution of the model, the optimal strategies of the attackers are calculated. Finally, the simulation tool is used to solve the feedback Nash equilibrium solution of the two players in the proposed model, and the experimental environment verifies the usability of the risk assessment method.

The contemporary struggle that rests upon security risk assessment of Information Systems is its feasibility in the presence of an indeterminate environment when information is insufficient, conflicting, generic or ambiguous. But as pointed out by the security experts, most of the traditional approaches to risk assessment of information systems security are no longer practicable as they fail to deliver viable support on handling uncertainty. Therefore, to address this issue, we have anticipated a comprehensive risk assessment model based on Bayesian Belief Network (BBN) and Fuzzy Inference Scheme (FIS) process to function in an indeterminate environment. The proposed model is demonstrated and further comparisons are made on the test results to validate the reliability of the proposed model.

Edge computing brings processing and storage capabilities closer to the data sources, to reduce network latency, save bandwidth, and preserve data locality. Despite the clear benefits, this paradigm brings unprecedented cyber risks due to the combination of the security issues and challenges typical of cloud and Internet of Things (IoT) worlds. Notwithstanding an increasing interest in edge security by academic and industrial communities, there is still no discernible industry consensus on edge computing security best practices, and activities like threat analysis and countermeasure selection are still not well established and are completely left to security experts.In order to cope with the need for a simplified yet effective threat modeling process, which is affordable in presence of limited security skills and economic resources, and viable in modern development approaches, in this paper, we propose an automated threat modeling and countermeasure selection strategy targeting edge computing systems. Our approach leverages a comprehensive system model able to describe the main involved architectural elements and the associated data flow, with a focus on the specific properties that may actually impact on the applicability of threats and of associated countermeasures.

This paper addresses security and risk management of hardware and embedded systems across several applications. There are three companies involved in the research. First is an energy technology company that aims to leverage electric- vehicle batteries through vehicle to grid (V2G) services in order to provide energy storage for electric grids. Second is a defense contracting company that provides acquisition support for the DOD's conventional prompt global strike program (CPGS). These systems need protections in their production and supply chains, as well as throughout their system life cycles. Third is a company that deals with trust and security in advanced logistics systems generally. The rise of interconnected devices has led to growth in systems security issues such as privacy, authentication, and secure storage of data. A risk analysis via scenario-based preferences is aided by a literature review and industry experts. The analysis is divided into various sections of Criteria, Initiatives, C-I Assessment, Emergent Conditions (EC), Criteria-Scenario (C-S) relevance and EC Grouping. System success criteria, research initiatives, and risks to the system are compiled. In the C-I Assessment, a rating is assigned to signify the degree to which criteria are addressed by initiatives, including research and development, government programs, industry resources, security countermeasures, education and training, etc. To understand risks of emergent conditions, a list of Potential Scenarios is developed across innovations, environments, missions, populations and workforce behaviors, obsolescence, adversaries, etc. The C-S Relevance rates how the scenarios affect the relevance of the success criteria, including cost, schedule, security, return on investment, and cascading effects. The Emergent Condition Grouping (ECG) collates the emergent conditions with the scenarios. The generated results focus on ranking Initiatives based on their ability to negate the effects of Emergent Conditions, as well as producing a disruption score to compare a Potential Scenario's impacts to the ranking of Initiatives. The results presented in this paper are applicable to the testing and evaluation of security and risk for a variety of embedded smart devices and should be of interest to developers, owners, and operators of critical infrastructure systems.

Approximate computing emerged as a key alternative for trading off accuracy against energy efficiency and area reduction. Error-tolerant applications, such as multimedia processing, machine learning, and signal processing, can process the information with lower-than-standard accuracy at the circuit level while still fulfilling a good and acceptable service quality at the application level. Adaptive filtering-based systems have been demonstrating high resiliency against hardware errors due to their intrinsic self-healing characteristic. This paper investigates the design space exploration of arithmetic approximations in a Very Large-Scale Integration (VLSI) harmonic elimination (HE) hardware architecture based on Least Mean Square (LMS) adaptive filters. We evaluate the Pareto front of the area- and power versus quality curves by relaxing the arithmetic precision and by adopting both approximate multipliers (AxMs) in combination with approximate adders (AxAs). This paper explores the benefits and impacts of the Dynamic Range Unbiased (DRUM), Rounding-based Approximate (RoBA), and Leading one Bit-based Approximate (LoBA) multipliers in the power dissipation, circuit area, and quality of the VLSI HE architectures. Our results highlight the LoBA 0 as the most efficient AxM applied in the HE architecture. We combine the LoBA 0 with Copy and LOA AxAs with variations in the approximation level (L). Notably, LoBA 0 and LOA with \$L=6\$ resulted in savings of 43.7% in circuit area and 45.2% in power dissipation, compared to the exact HE, which uses multiplier and adder automatically selected by the logic synthesis tool. Finally, we demonstrate that the best hardware architecture found in our investigation successfully eliminates the contaminating spurious noise (i.e., 60 Hz and its harmonics) from the signal.

This paper presents a new framework for SATCOM jamming resiliency in the presence of a smart adversary jammer that can prioritize specific channels to attack with a non-uniform probability of distribution. We first develop a model and a defense action strategy based on a Markov decision process (MDP). We propose a greedy algorithm for the MDP-based defense algorithm's policy to optimize the expected user's immediate and future discounted rewards. Next, we remove the assumption that the user has specific information about the attacker's pattern and model. We develop a Q-learning algorithm-a reinforcement learning (RL) approach-to optimize the user's policy. We show that the Q-learning method provides an attractive defense strategy solution without explicit knowledge of the jammer's strategy. Computer simulation results show that the MDP-based defense strategies are very efficient; they offer a significant data rate advantage over the simple random hopping approach. Also, the proposed Q-learning performance can achieve close to the MDP approach without explicit knowledge of the jammer's strategy or attacking model.

Mobile antivirus technologies incorporate static analysis which involves the analysis of programs without its execution. This process relies on pattern matching against a signature repository to identify malware, which can be easily tricked by transformation techniques such as obfuscation. Obfuscation as an evasion technique renders character strings disguised and incomprehensive, to prevent tampering and reengineering, which poses to be a valuable technique malware developers adopt to evade detection. This paper attempts to study the detection efficiency of static analyzers against obfuscated Android malware. This study is the first step in a larger project attempting to improve the efficiency of malware detectors.

Fix pattern-based patch generation is a promising direction in Automated Program Repair (APR). Notably, it has been demonstrated to produce more acceptable and correct patches than the patches obtained with mutation operators through genetic programming. The performance of pattern-based APR systems, however, depends on the fix ingredients mined from fix changes in development histories. Unfortunately, collecting a reliable set of bug fixes in repositories can be challenging. In this paper, we propose to investigate the possibility in an APR scenario of leveraging code changes that address violations by static bug detection tools. To that end, we build the AVATAR APR system, which exploits fix patterns of static analysis violations as ingredients for patch generation. Evaluated on the Defects4J benchmark, we show that, assuming a perfect localization of faults, AVATAR can generate correct patches to fix 34/39 bugs. We further find that AVATAR yields performance metrics that are comparable to that of the closely-related approaches in the literature. While AVATAR outperforms many of the state-of-the-art pattern-based APR systems, it is mostly complementary to current approaches. Overall, our study highlights the relevance of static bug finding tools as indirect contributors of fix ingredients for addressing code defects identified with functional test cases.

One of the major issues which are hindering widespread and seamless adoption of Internet of Thing (IoT) is security. The IoT devices are vulnerable and susceptible to attacks which became evident from a series of recent large-scale distributed denial-of-service (DDoS) attacks, leading to substantial business and financial losses. Furthermore, in order to find vulnerabilities in IoT, there is a lack of comprehensive security analysis framework. In this paper, we present a modular, adaptable and tunable framework, called PIT, to probe IoT systems at different layers of design and implementation. PIT consists of several security analysis engines, viz., penetration testing, fuzzing, static analysis, and dynamic analysis and an exploitation engine to discover multiple IoT vulnerabilities, respectively. We also develop a novel grey-box fuzzer, called Applica, as a part of the fuzzing engine to overcome the limitations of the present day fuzzers. The proposed framework has been evaluated on a real-world IoT testbed comprising of the state-of-the-art devices. We discovered several network and system-level vulnerabilities such as Buffer Overflow, Denial-of-Service, SQL Injection, etc., and successfully exploited them to demonstrate the presence of security loopholes in the IoT devices.

Static analysis tools are programs that run on source code prior to their compilation to binary executables and attempt to find flaws or defects in the code during the early stages of development. If left unresolved, these flaws could pose security risks. While numerous static analysis tools exist, there is no single tool that is optimal. Therefore, many static analysis tools are often used to analyze code. Further, some of the alerts generated by the static analysis tools are low-priority or false alarms. Machine learning algorithms have been developed to distinguish between true alerts and false alarms, however significant man hours need to be dedicated to labeling data sets for training. This study investigates the use of active learning to reduce the number of labeled alerts needed to adequately train a classifier. The numerical experiments demonstrate that a query by committee active learning algorithm can be utilized to significantly reduce the number of labeled alerts needed to achieve similar performance as a classifier trained on a data set of nearly 60,000 labeled alerts.

Visual Question Answering (VQA) models have achieved significant success in recent times. Despite the success of VQA models, they are mostly black-box models providing no reasoning about the predicted answer, thus raising questions for their applicability in safety-critical such as autonomous systems and cyber-security. Current state of the art fail to better complex questions and thus are unable to exploit compositionality. To minimize the black-box effect of these models and also to make them better exploit compositionality, we propose a Dynamic Neural Network (DMN), which can understand a particular question and then dynamically assemble various relatively shallow deep learning modules from a pool of modules to form a network. We incorporate compositional temporal attention to these deep learning based modules to increase compositionality exploitation. This results in achieving better understanding of complex questions and also provides reasoning as to why the module predicts a particular answer. Experimental analysis on the two benchmark datasets, VQA2.0 and CLEVR, depicts that our model outperforms the previous approaches for Visual Question Answering task as well as provides better reasoning, thus making it reliable for mission critical applications like safety and security.

Recent projects regarding the exploration of the functions of microbiomes within communities brought about a plethora of new data. That specific field of study is called Metagenomics and one of its more advancing approach is the application of network analysis. The paper introduces NAMData which is a web-application tool for the network analysis of microbiome data. The system handles the compositionality and sparsity nature of microbiome data by applying taxa filtration, normalization, and zero treatment. Furthermore, compositionally aware correlation estimators were used to compute for the correlation between taxa and the system divides the network into the positive and negative correlation network. NAMData aims to capitalize on the unique network features namely network visualization, centrality scores, and community detection. The system enables researchers to include network analysis in their analysis pipelines even without any knowledge of programming. Biological concepts can be integrated with the network findings gathered from the system to either support existing facts or form new insights.

While language learning in infants and toddlers progresses somewhat seamlessly, in artificial systems the grounding of language in knowledge structures that are learned from sensorimotor experiences remains a hard challenge. Here we introduce LEARNA, which learns event-characterizing abstractions to resolve natural language ambiguity. LEARNA develops knowledge structures from simulated sensorimotor experiences. Given a possibly ambiguous descriptive utterance, the learned knowledge structures enable LEARNA to infer environmental scenes, and events unfolding within, which essentially constitute plausible imaginations of the utterance’s content. Similar event-predictive structures may help in developing artificial systems that can generate and comprehend descriptions of scenes and events.

A kitchen underpinned by the Internet of Things (IoT) requires the management of complex procedural processes. This is due to the fact that when supporting an end-user in the preparation of even only one dish, various devices may need to coordinate with each other. Additionally, it is challenging— yet desirable—to enable an end-user to program their kitchen devices according to their preferred behaviour and to allow them to visualise and track their cooking workflows. In this paper, we compared two semantic representations, namely, Behaviour Trees and the DX-MAN model. We analysed these representations based on their suitability for a range of end-users (i.e., novice to experienced). The methodology required the analysis of smart kitchen user requirements, from which we inferred that the main architectural requirements for IoT cooking workflows are variability and compositionality. Guided by the user requirements, we examined various scenarios and analysed workflow complexity and feasibility for each representation. On the one hand, we found that execution complexity tends to be higher on Behaviour Trees. However, due to their fallback node, they provide more transparency on how to recover from unprecedented circumstances. On the other hand, parameter complexity tends to be somewhat higher for the DX-MAN model. Nevertheless, the DX-MAN model can be favourable due to its compositionality aspect and the ease of visualisation it can offer.

Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.