Open Access. Powered by Scholars. Published by Universities.®
- Institution
Articles 1 - 14 of 14
Full-Text Articles in Entire DC Network
Formally Designing And Implementing Cyber Security Mechanisms In Industrial Control Networks., Mehdi Sabraoui
Formally Designing And Implementing Cyber Security Mechanisms In Industrial Control Networks., Mehdi Sabraoui
Electronic Theses and Dissertations
This dissertation describes progress in the state-of-the-art for developing and deploying formally verified cyber security devices in industrial control networks. It begins by detailing the unique struggles that are faced in industrial control networks and why concepts and technologies developed for securing traditional networks might not be appropriate. It uses these unique struggles and examples of contemporary cyber-attacks targeting control systems to argue that progress in securing control systems is best met with formal verification of systems, their specifications, and their security properties. This dissertation then presents a development process and identifies two technologies, TLA+ and seL4, that can be …
Testing The Fault Tolerance Of A Wide Area Backup Protection System Using Spin, Kenneth James
Testing The Fault Tolerance Of A Wide Area Backup Protection System Using Spin, Kenneth James
Theses and Dissertations
Cyber-physical systems are increasingly prevalent in daily life. Smart grids in particular are becoming more interconnected and autonomously operated. Despite the advantages, new challenges arise in the form of defending these assets. Recent studies reveal that small-scale, coordinated cyber-attacks on only a few substations across the U.S. could result in cascading failures affecting the entire nation. In support of defending critical infrastructure, this thesis tests the fault tolerance of a backup protection system. Each transmission line in the system incorporates autonomous agents which monitor the status of the line and make decisions regarding the safety of the grid. Various malfunctions …
Specification And Analysis Of Resource Utilization Policies For Human-Intensive Systems, Seung Yeob Shin
Specification And Analysis Of Resource Utilization Policies For Human-Intensive Systems, Seung Yeob Shin
Doctoral Dissertations
Contemporary systems often require the effective support of many types of resources, each governed by complex utilization policies. Sound management of these resources plays a key role in assuring that these systems achieve their key goals. To help system developers make sound resource management decisions, I provide a resource utilization policy specification and analysis framework for (1) specifying very diverse kinds of resources and their potentially complex resource utilization policies, (2) dynamically evaluating the policies’ effects on the outcomes achieved by systems utilizing the resources, and (3) formally verifying various kinds of properties of these systems. Resource utilization policies range …
Verification Of Task Parallel Programs Using Predictive Analysis, Radha Vi Nakade
Verification Of Task Parallel Programs Using Predictive Analysis, Radha Vi Nakade
Theses and Dissertations
Task parallel programming languages provide a way for creating asynchronous tasks that can run concurrently. The advantage of using task parallelism is that the programmer can write code that is independent of the underlying hardware. The runtime determines the number of processor cores that are available and the most efficient way to execute the tasks. When two or more concurrently executing tasks access a shared memory location and if at least one of the accesses is for writing, data race is observed in the program. Data races can introduce non-determinism in the program output making it important to have data …
An Analyzer For Message Passing Programs, Yu Huang
An Analyzer For Message Passing Programs, Yu Huang
Theses and Dissertations
Asynchronous message passing systems are fast becoming a common means for communication between devices. Two problems existing in message passing programs are difficult to solve. The first problem, intended or otherwise, is message-race where a receive may match with more than one send in the runtime system. This non-determinism often leads to intermittent and unexpected behavior depending on the resolution of the race. Another problem is deadlock, which is a situation in that each member process of the group is waiting for some member process to communicate with it, but no member is attempting to communicate with it. Detecting if …
Maintaining Consistency Between A Design Model And Its Implementation, Hector M. Chavez
Maintaining Consistency Between A Design Model And Its Implementation, Hector M. Chavez
Dissertations
Software design models are increasingly being used as part of the software development process as analysis and design artifacts and to automatically generate code that developers can further modify or extend, greatly expediting the software development process. This, however, has introduced the challenge of maintaining consistency between the design models and their implementation as they evolve during the development process. Traditional software testing and verification techniques have been well studied in the past, and they are an integral part of many software development projects, however, they are not well suited for consistency checking between a design model and its implementation. …
Verifying Abstract Components Within Concrete Software Environments, Tonglaga Bao
Verifying Abstract Components Within Concrete Software Environments, Tonglaga Bao
Theses and Dissertations
In order to model check a software component which is not a standalone program, we need a model of the software which completes the program. This problem is important for software engineers who need to deploy an existing component into a new environment. The model is typically generated by abstracting the surrounding software environment in which the component will be executed. However, abstracting the surrounding software is a difficult and error-prone task, particularly when the surrounding software is a complex software artifact which can not be easily abstracted. In this dissertation, we present a new approach to the problem by …
Using Live Sequence Chart Specifications For Formal Verification, Rahul Kumar
Using Live Sequence Chart Specifications For Formal Verification, Rahul Kumar
Theses and Dissertations
Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a …
Machine Code Verification Using The Bogor Framework, Joseph R. Edelman
Machine Code Verification Using The Bogor Framework, Joseph R. Edelman
Theses and Dissertations
Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an "off-the-shelf" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features …
Finding Termination And Time Improvement In Predicate Abstraction With Under-Approximation And Abstract Matching, Dritan Kudra
Finding Termination And Time Improvement In Predicate Abstraction With Under-Approximation And Abstract Matching, Dritan Kudra
Theses and Dissertations
The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. …
On-The-Fly Dynamic Dead Variable Analysis, Joel P. Self
On-The-Fly Dynamic Dead Variable Analysis, Joel P. Self
Theses and Dissertations
State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover …
Improving Error Discovery Using Guided Model Checking, Neha Shyam Rungta
Improving Error Discovery Using Guided Model Checking, Neha Shyam Rungta
Theses and Dissertations
State exploration in directed software model checking is guided using a heuristic function to move states near errors to the front of the search queue. Distance heuristic functions rank states based on the number of transitions needed to move the current program state into an error location. Lack of calling context information causes the heuristic function to underestimate the true distance to the error; however, inlining functions at call sites in the control flow graph to capture calling context leads to exponential growth in the computation. This paper presents a new algorithm that implicitly inlines functions at call sites to …
Dynamic Dead Variable Analysis, Micah S. Lewis
Dynamic Dead Variable Analysis, Micah S. Lewis
Theses and Dissertations
Dynamic dead variable analysis (DDVA) extends traditional static dead variable analysis (SDVA) in the context of model checking through the use of run-time information. The analysis is run multiple times during the course of model checking to create a more precise set of dead variables. The DDVA is evaluated based on the amount of memory used to complete model checking relative to SDVA while considering the extra overhead required to implement DDVA. On several models with a complex control flow graph, DDVA reduces the amount of memory needed by 38-88MB compared to SDVA with a cost of 36 bytes of …
January: Search Based On Social Insect Behavior, Peter C. Lamborn
January: Search Based On Social Insect Behavior, Peter C. Lamborn
Theses and Dissertations
January is a group of interacting stateless model checkers. Each agent functions on a processor located on a super computer or a network of workstations (NOW). The agent's search pattern is a semi-random walk based on the behavior of the grey field slug (Agriolimax reticulatus), the house fly (Musca domestica), and the black ant (Lassius niger). The agents communicate to lessen the amount of duplicate work being done. Every algorithm has a memory threshold above which they search efficiently. This threshold varies not only by model but also by algorithm. Janaury's threshold is lower than the thresholds of other algorithms …