Biblio
The modern world is becoming increasingly dependent on computing and communication technology to function, but unfortunately its application and impact on areas such as critical infrastructure and industrial control system (ICS) networks remains to be thoroughly studied. Significant research has been conducted to address the myriad security concerns in these areas, but they are virtually all based on artificial testbeds or simulations designed on assumptions about their behavior either from knowledge of traditional IT networking or from basic principles of ICS operation. In this work, we provide the most detailed characterization of an example ICS to date in order to determine if these common assumptions hold true. A live power distribution substation is observed over the course of two and a half years to measure its behavior and evolution over time. Then, a horizontal study is conducted that compared this behavior with three other substations from the same company. Although most predictions were found to be correct, some unexpected behavior was observed that highlights the fundamental differences between ICS and IT networks including round trip times dominated by processing speed as opposed to network delay, several well known TCP features being largely irrelevant, and surprisingly large jitter from devices running real-time operating systems. The impact of these observations is discussed in terms of generality to other embedded networks, network security applications, and the suitability of the TCP protocol for this environment.
During its nascent stages, Programmable Logic Controllers (PLC) were made robust to sustain tough industrial environments, but little care was taken to raise defenses against potential cyberthreats. The recent interconnectivity of legacy PLCs and SCADA systems with corporate networks and the internet has significantly increased the threats to critical infrastructure. To counter these threats, researchers have put their efforts in finding defense mechanisms that can protect the SCADA network and the PLCs. Encryption is a critical component of security and therefore has been used by many organizations to protect data on the network. However, since PLC vendors don't make available information about their hardware or software, it becomes challenging to embed encryption into their devices, especially if they rely on legacy protocols. This paper describes an alternative design using an open source PLC that was modified to encrypt all data it sends over the network, independently of the protocol used. Experimental results indicated that the encryption layer increased the security of the link without causing a significant overhead.
The SCADA infrastructure is a key component for power grid operations. Securing the SCADA infrastructure against cyber intrusions is thus vital for a well-functioning power grid. However, the task remains a particular challenge, not the least since not all available security mechanisms are easily deployable in these reliability-critical and complex, multi-vendor environments that host modern systems alongside legacy ones, to support a range of sensitive power grid operations. This paper examines how effective a few countermeasures are likely to be in SCADA environments, including those that are commonly considered out of bounds. The results show that granular network segmentation is a particularly effective countermeasure, followed by frequent patching of systems (which is unfortunately still difficult to date). The results also show that the enforcement of a password policy and restrictive network configuration including whitelisting of devices contributes to increased security, though best in combination with granular network segmentation.
The exploitation of Industrial Control Systems (ICSs) has been described as both easy and impossible, where is the truth? PostStuxnet works have included a plethora of ICS focused cyber security research activities, with topics covering device maturity, network protocols, and overall cyber security culture. We often hear the notion of ICSs being highly vulnerable due to a lack of inbuilt security mechanisms, considered a low hanging fruit to a variety of low skilled threat actors. While there is substantial evidence to support such a notion, when considering targeted attacks on ICS, it is hard to believe an attacker with limited resources, such as a script kiddie or hacktivist, using publicly accessible tools and exploits alone, would have adequate knowledge and resources to achieve targeted operational process manipulation, while simultaneously evade detection. Through use of a testbed environment, this paper provides two practical examples based on a Man-In-The-Middle scenario, demonstrating the types of information an attacker would need obtain, collate, and comprehend, in order to begin targeted process manipulation and detection avoidance. This allows for a clearer view of associated challenges, and illustrate why targeted ICS exploitation might not be possible for every malicious actor.
Despite significant recent advances, the effectiveness of symbolic execution is limited when used to test complex, real-world software. One of the main scalability challenges is related to constraint solving: large applications and long exploration paths lead to complex constraints, often involving big arrays indexed by symbolic expressions. In this paper, we propose a set of semantics-preserving transformations for array operations that take advantage of contextual information collected during symbolic execution. Our transformations lead to simpler encodings and hence better performance in constraint solving. The results we obtain are encouraging: we show, through an extensive experimental analysis, that our transformations help to significantly improve the performance of symbolic execution in the presence of arrays. We also show that our transformations enable the analysis of new code, which would be otherwise out of reach for symbolic execution.
Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology.
Two known shortcomings of standard techniques in formal verification are the limited capability to provide system-level assertions, and the scalability to large, complex models, such as those needed in Cyber-Physical Systems (CPS) applications. Leveraging data, which nowadays is becoming ever more accessible, has the potential to mitigate such limitations. However, this leads to a lack of formal proofs that are needed for modern safety-critical systems. This contribution presents a research initiative that addresses these shortcomings by bringing model-based techniques and data-driven methods together, which can help pushing the envelope of existing algorithms and tools in formal verification and thus expanding their applicability to complex engineering systems, such as CPS. In the first part of the contribution, we discuss a new, formal, measurement-driven and model-based automated technique, for the quantitative verification of physical systems with partly unknown dynamics. We formulate this setup as a data-driven Bayesian inference problem, formally embedded within a quantitative, model-based verification procedure. We argue that the approach can be applied to complex physical systems that are key for CPS applications, dealing with spatially continuous variables, evolving under complex dynamics, driven by external inputs, and accessed under noisy measurements. In the second part of the contribution, we concentrate on systems represented by models that evolve under probabilistic and heterogeneous (continuous/discrete - that is "hybrid" - as well as nonlinear) dynamics. Such stochastic hybrid models (also known as SHS) are a natural mathematical framework for CPS. With focus on model-based verification procedures, we provide algorithms for quantitative model checking of temporal specifications on SHS with formal guarantees. This is attained via the development of formal abstraction techniques that are based on quantitative approximations. Theory is complemented by algorithms, all packaged in software tools that are available to users, and which are applied here in the domain of Smart Energy.
Developing Big Data Analytics workloads often involves trial and error debugging, due to the unclean nature of datasets or wrong assumptions made about data. When errors (e.g., program crash, outlier results, etc.) arise, developers are often interested in identifying a subset of the input data that is able to reproduce the problem. BigSift is a new faulty data localization approach that combines insights from automated fault isolation in software engineering and data provenance in database systems to find a minimum set of failure-inducing inputs. BigSift redefines data provenance for the purpose of debugging using a test oracle function and implements several unique optimizations, specifically geared towards the iterative nature of automated debugging workloads. BigSift improves the accuracy of fault localizability by several orders-of-magnitude ($\sim$103 to 107×) compared to Titian data provenance, and improves performance by up to 66× compared to Delta Debugging, an automated fault-isolation technique. For each faulty output, BigSift is able to localize fault-inducing data within 62% of the original job running time.
We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of network functions and proves properties specific to network configuration, such as reachability and absence of loops. Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs. Prior work argued that this is not feasible (i.e., that verifying a real, stateful network function written in C does not scale) but we demonstrate otherwise: NAT is one of the most popular network functions and maintains per-flow state that needs to be properly updated and expired, which is a typical source of verification challenges. We tackle the scalability challenge with a new combination of symbolic execution and proof checking using separation logic; this combination matches well the typical structure of a network function. We then demonstrate that formally proven correctness in this case does not come at the cost of performance. The NAT code, proof toolchain, and proofs are available at [58].
Fuzzing is a software testing technique that finds bugs by repeatedly injecting mutated inputs to a target program. Known to be a highly practical approach, fuzzing is gaining more popularity than ever before. Current research on fuzzing has focused on producing an input that is more likely to trigger a vulnerability. In this paper, we tackle another way to improve the performance of fuzzing, which is to shorten the execution time of each iteration. We observe that AFL, a state-of-the-art fuzzer, slows down by 24x because of file system contention and the scalability of fork() system call when it runs on 120 cores in parallel. Other fuzzers are expected to suffer from the same scalability bottlenecks in that they follow a similar design pattern. To improve the fuzzing performance, we design and implement three new operating primitives specialized for fuzzing that solve these performance bottlenecks and achieve scalable performance on multi-core machines. Our experiment shows that the proposed primitives speed up AFL and LibFuzzer by 6.1 to 28.9x and 1.1 to 735.7x, respectively, on the overall number of executions per second when targeting Google's fuzzer test suite with 120 cores. In addition, the primitives improve AFL's throughput up to 7.7x with 30 cores, which is a more common setting in data centers. Our fuzzer-agnostic primitives can be easily applied to any fuzzer with fundamental performance improvement and directly benefit large-scale fuzzing and cloud-based fuzzing services.
This work describes how automated data generation integrates in a big data pipeline. A lack of veracity in big data can cause models that are inaccurate, or biased by trends in the training data. This can lead to issues as a pipeline matures that are difficult to overcome. This work describes the use of a Generative Adversarial Network to generate sketch data, such as those that might be used in a human verification task. These generated sketches are verified as recognizable using a crowd-sourcing methodology, and finds that the generated sketches were correctly recognized 43.8% of the time, in contrast to human drawn sketches which were 87.7% accurate. This method is scalable and can be used to generate realistic data in many domains and bootstrap a dataset used for training a model prior to deployment.
WBANs integrate wearable and implanted devices with wireless communication and information processing systems to monitor the well-being of an individual. Various MAC (Medium Access Control) protocols with different objectives have been proposed for WBANs. The fact that any flaw in these critical systems may lead to the loss of one's life implies that testing and verifying MAC's protocols for such systems are on the higher level of importance. In this paper, we firstly propose a high-level formal and scalable model with timing aspects for a MAC protocol particularly designed for WBANs, named S-TDMA (Statistical frame based TDMA protocol). The protocol uses TDMA (Time Division Multiple Access) bus arbitration, which requires temporal aspect modeling. Secondly, we propose a formal validation of several relevant properties such as deadlock freedom, fairness and mutual exclusion of this protocol at a high level of abstraction. The protocol was modeled using a composition of timed automata components, and verification was performed using a real-time model checker.
Vectorless integrity verification is becoming increasingly critical to robust design of nanoscale power delivery networks (PDNs). To dramatically improve efficiency and capability of vectorless integrity verifications, this paper introduces a scalable multilevel integrity verification framework by leveraging a hierarchy of almost linear-sized spectral power grid sparsifiers that can well retain effective resistances between nodes, as well as a recent graph-theoretic algebraic multigrid (AMG) algorithmic framework. As a result, vectorless integrity verification solution obtained on coarse level problems can effectively help find the solution of the original problem. Extensive experimental results show that the proposed vectorless verification framework can always efficiently and accurately obtain worst-case scenarios in even very large power grid designs.
To reduce the complex communication problem that arise as the number of on-chip component increases, the use of Network-on-Chip (NoC) as interconnection architectures have become more promising to solve complex on-chip communication problems. However, providing a suitable test base to measure and verify functionality of any NoC is a compulsory. Universal Verification Methodology (UVM) is introduced as a standardized and reusable methodology for verifying integrated circuit design. In this research, a scalable and reconfigurable verification and benchmark environment for NoC is proposed.
With the rapid development of sophisticated attack techniques, individual security systems that base all of their decisions and actions of attack prevention and response on their own observations and knowledge become incompetent. To cope with this problem, collaborative security in which a set of security entities are coordinated to perform specific security actions is proposed in literature. In collaborative security schemes, multiple entities collaborate with each other by sharing threat evidence or analytics to make more effective decisions. Nevertheless, the anticipated information exchange raises privacy concerns, especially for those privacy-sensitive entities. In order to obtain a quantitative understanding of the fundamental tradeoff between the effectiveness of collaboration and the entities' privacy, a repeated two-layer single-leader multi-follower game is proposed in this work. Based on our game-theoretic analysis, the expected behaviors of both the attacker and the security entities are derived and the utility-privacy tradeoff curve is obtained. In addition, the existence of Nash equilibrium (NE) for the collaborative entities is proven, and an asynchronous dynamic update algorithm is proposed to compute the optimal collaboration strategies of the entities. Furthermore, the existence of Byzantine entities is considered and its influence is investigated. Finally, simulation results are presented to validate the analysis.
Reliable operation of electrical power systems in the presence of multiple critical N - k contingencies is an important challenge for the system operators. Identifying all the possible N - k critical contingencies to design effective mitigation strategies is computationally infeasible due to the combinatorial explosion of the search space. This paper describes two heuristic algorithms based on the iterative pruning of the candidate contingency set to effectively and efficiently identify all the critical N - k contingencies resulting in system failure. These algorithms are applied to the standard IEEE-14 bus system, IEEE-39 bus system, and IEEE-57 bus system to identify multiple critical N - k contingencies. The algorithms are able to capture all the possible critical N - k contingencies (where 1 ≤ k ≤ 9) without missing any dangerous contingency.
Mobile ad-hoc network (MANET) contains various wireless movable nodes which can communicate with each other and they don't require any centralized administrator or network infrastructure and also can communicate with full capacity because it is composed of mobile nodes. They transmit data to each other with the help of intermediate nodes by establishing a path. But sometime malicious node can easily enter in network due to the mobility of nodes. That malicious node can harm the network by dropping the data packets. These type of attack is called gray hole attack. For detection and prevention from this type of attack a mechanism is proposed in this paper. By using network simulator, the simulation will be carried out for reporting the difficulties of prevention and detection of multiple gray hole attack in the Mobile ad-hoc network (MANET). Particle Swarm Optimization is used in this paper. Because of ad-hoc nature it observers the changing values of the node, if the value is infinite then node has been attacked and it prevents other nodes from sending data to that node. In this paper, we present possible solutions to prevent the network. Firstly, find more than one route to transmit packets to destination. Second, we provide minimum time delay to deliver the packet. The simulation shows the higher throughput, less time delay and less packet drop.
Fog computing provides a new architecture for the implementation of the Internet of Things (IoT), which can connect sensor nodes to the cloud using the edge of the network. This structure has improved the latency and energy consumption in the cloud. In this heterogeneous and distributed environment, resource allocation is very important. Hence, scheduling will be a challenge to increase productivity and allocate resources appropriately to the tasks. Programs that run in this environment should be protected from intruders. We consider three parameters as authentication, integrity, and confidentiality to maintain security in fog devices. These parameters have time and computational overhead. In the proposed approach, we schedule the modules for the run in fog devices by heuristic algorithms based on data mining technique. The objective function is included CPU utilization, bandwidth, and security overhead. We compare the proposed algorithm with several heuristic algorithms. The results show that our proposed algorithm improved the average energy consumption of 63.27%, cost 44.71% relative to the PSO, ACO, SA algorithms.
The continuous advance in recent cloud-based computer networks has generated a number of security challenges associated with intrusions in network systems. With the exponential increase in the volume of network traffic data, involvement of humans in such detection systems is time consuming and a non-trivial problem. Secondly, network traffic data tends to be highly dimensional, comprising of numerous features and attributes, making classification challenging and thus susceptible to the curse of dimensionality problem. Given such scenarios, the need arises for dimensional reduction, feature selection, combined with machine-learning techniques in the classification of such data. Therefore, as a contribution, this paper seeks to employ data mining techniques in a cloud-based environment, by selecting appropriate attributes and features with the least importance in terms of weight for the classification. Often the standard is to select features with better weights while ignoring those with least weights. In this study, we seek to find out if we can make prediction using those features with least weights. The motivation is that adversaries use stealth to hide their activities from the obvious. The question then is, can we predict any stealth activity of an adversary using the least observed attributes? In this particular study, we employ information gain to select attributes with the lowest weights and then apply machine learning to classify if a combination, in this case, of both source and destination ports are attacked or not. The motivation of this investigation is if attributes that are of least importance can be used to predict if an attack could occur. Our preliminary results show that even when the source and destination port attributes are used in combination with features with the least weights, it is possible to classify such network traffic data and predict if an attack will occur or not.