Doctor of Philosophy, The Ohio State University, 2024, Computer Science and Engineering

Software and protocol development has followed the design-develop-break-patch cycle for many years. One resolution to mitigate such a persistent cycle is to build the systems with formal analysis following the "analysis-prior-to-development'' philosophy. At present, state space explosion and the limited expressibility of formal model languages limit the scalability and efficiency of this approach. Expanding the scope of formal methods to broader cases requires augmented modeling and a deeper understanding of the underlying operating mechanisms. In particular, by modeling with a precise system environment and refined adversary capabilities, I wish to expand the boundaries of formal methods, exposing limiting root causes and opening novel paths for improvement. For example, considering how concurrent execution influences the processes; modeling a granular access control for user and adversary groups; incorporating human interactions; allowing adversaries to control program execution at the instruction level; and trading off between literal cryptographic accuracy and modeled theory imprecisions augments the formal modeling to reason about unconventional properties. Apart from raising security assurance, such comprehensive coverage of the system environment and precise adversary capability expand the utility of formal methods to large systems and facilitate the derivation of unconventional properties. Additionally, such design provides further feedback to formal tool development to design targeted building blocks that improve the efficiency, scalability, and expressibility of formal modeling. In this thesis, I first present an enhanced and generic formal analysis of the trusted execution environment (TEE) technology -- Software Guard Extension -- built by Intel. In particular, I made a first attempt toward extending formal verification to program logic for SGX enclaves with the powerful SGX threat model. In this effort, I derived state continuity properties with r (open full item for complete abstract)

Committee: Zhiqiang Lin (Advisor); Feng Qin (Committee Member); Carter Yagemann (Committee Member); Srinivasan Parthasarathy (Committee Member); David Landsbergen (Other) Subjects: Computer Engineering; Computer Science

Doctor of Philosophy, The Ohio State University, 2024, Computer Science and Engineering

Unmanned Aerial Systems (UAS) are increasingly important. Farmers monitor crops and apply pesticides with UAS. First responders use UAS in applications ranging from fire fighting to search and rescue operations. There is potential for rapid shopping delivery by UAS. In all these applications, UAS work closely alongside humans. Onboard firmware controls the behavior of UAS. This dissertation studies ways to improve the quality of firmware. We start by presenting the first large-scale analysis of software defects ("bugs") reported in open-source UAS firmware. We examine nearly 300 reported bugs in the two most popular open-source systems (ArduPilot and PX4) and categorize the defects. Motivated by our findings, we propose three technologies to automate the detection and repair of UAS bugs. First, Avis seeks to automatically diagnose sensor bugs caused by misusing onboard sensors. Second, SA4U identifies unit type errors caused by incorrectly mixing values with different physical unit types (e.g., meters and minutes) in a computation. Finally, Scalpel automatically repairs bugs found by SA4U. Deep learning is increasingly used to provide advanced autonomous behavior for UAS. To support higher quality deep learning systems we propose checkd. Checkd automates checkpoint/restore policy configurations. Underlying checkd's contribution is the thesis that better tuned models yield better behavior. Checkd helps practitioners fine-tune models by reducing the overall cost to train.

Committee: Feng Qin (Advisor); Michael Bond (Committee Member); Christopher Stewart (Committee Member) Subjects: Computer Science

Bachelor of Science (BS), Ohio University, 2022, Mathematics

The increasing scale and complexity of mathematics brings with it concerns on how to efficiently validate new results. Proof assistants offer a compelling solution, but the task of formalizing results in these languages often requires immense effort and practice. Autoformalization attempts to address this by automatically translating informal proofs into a formal language, generally a proof assistant. This report pro- poses and evaluates a set of neural encoder-decoder models based on the Transformer architecture for the task of autoformalization. We create a dataset of mathematical proofs typeset in LaTeX with paired programs written in the Coq proof assistant for training and evaluation. To our knowledge, this is the first report to test performance on full proofs. Additionally, we extend our approach to proofs about program correctness, which is currently unexplored in the literature. Experimental results show that our models perform well on our selected data and are able to generalize to lengths not seen during training.

Committee: David Juedes (Advisor) Subjects: Computer Science; Mathematics

PhD, University of Cincinnati, 2021, Engineering and Applied Science: Computer Science and Engineering

Verification and validation are very important in the design of any system. For safety-critical systems, especially, the validation level is crucial. In this work, developing a robust procedure for designing smart, safe, secure systems is our eventual goal. There are different methods for verification and validation, but formal methods are used widely to validate these systems due to their high level of confidence for guaranteeing correctness, security, and safety properties. TLA+ is a formal specification language and its TLC model checker will be used in this work to formally verify and validate several example systems, and to find security hacks. Designing smart systems has recently received much attention because of the ability to connect heterogeneous sub-systems together to build a fully controlled smart system. Here we propose models for three systems: a smart school building system, an ADS-B system for avionics, and a SCADA system. We model the systems using UML diagrams to describe objects, states, and sequences of actions. Formal methods techniques are used to verify the properties of the systems. TLA+ is used for formal modeling. For the smart school building system, the ADS-B system, and the SCADA system, we verify their properties and correctness using the TLA+ toolbox and the TLC model checker. Also, we use the TLC model checker to find example security bugs we introduce into the designs.

Committee: Carla Purdy Ph.D. (Committee Chair); Shaaban Abdallah Ph.D. (Committee Member); Nan Niu Ph.D. (Committee Member); Massoud (Max) Rabiee Ph.D. (Committee Member); Boyang Wang (Committee Member) Subjects: Computer Engineering

Master of Science (MS), Wright State University, 2018, Computer Science

Data-Oriented Programming (DOP) is a data-only code-reuse exploit technique that “stitches” together sequences of instructions to alter a program's data flow to cause harm. DOP attacks are difficult to mitigate because they respect the legitimate control flow of a program and by-pass memory protection schemes such as Address Space Layout Randomization, Data Execution Prevention, and Control Flow Integrity. Techniques that describe how to build DOP payloads rely on a program's source code. This research explores the feasibility of constructing DOP exploits without source code—that is, using only binary representations of programs. The lack of semantic and type information introduces difficulties in identifying data-oriented gadgets and their properties. This research uses binary program analysis techniques and formal methods to identify and verify data-oriented gadgets, and determine if they are reachable and executable from a given memory corruption vulnerability. This information guides the construction of DOP attacks without the need for source code, showing that common-off-the-shelf programs are also vulnerable to this class of exploit.

Committee: Adam Bryant Ph.D. (Committee Co-Chair); John Emmert Ph.D. (Committee Co-Chair); Meilin Liu Ph.D. (Committee Member); Krishnaprasad Thirunarayan Ph.D. (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2016, Computer Science and Engineering

Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing this long-standing verification problem try not to sacrifice modularity because modular reasoning is what makes verification tractable. To achieve this, these approaches treat the value of a reference variable as a memory address in the heap. A serious problem with this decision is that it severely limits the usefulness of generic collections because they must be specified as collections of references, and components of this kind are fundamentally flawed in design and implementation. The limitations become clear when attempting to verify clients of generic collections. The first step in rectifying the situation is to redefine the "value" of a reference variable in terms of the abstract value of the object it references. A careful analysis of what the "value" of a reference variable might mean leads inevitably to this conclusion, which is consistent with the denotation of a variable in languages with value semantics, such as RESOLVE. Verification in languages with value semantics is straightforward compared to verification in languages with reference semantics precisely because of the lack of concern with heap properties. However, there is still a nagging problem: aliasing can occur in legal programs in languages with reference semantics, such as Java, and it must be handled when it does occur. The crux of the issue is not in-your-face assignment statements that copy references but rather aliasing arising within (hidden) method bodies. The reason is that the effects of calls to these methods in client code must be summarized in their specifications in order to preserve modularity. So, the second step is the introduction of a discipline restricting what a client can do with a reference that is aliased within a method. The discipline advertises the creation of such aliases in method speci (open full item for complete abstract)

Committee: Bruce W. Weide (Advisor); Neelam Soundarajan (Committee Member); Paul A. G. Sivilotti (Committee Member) Subjects: Computer Science

Master of Science in Software Engineering, Cleveland State University, 2014, Washkewicz College of Engineering

FreeRTOS is a popular real-time and embedded operating system. Real-time software requires code reviews, software tests, and other various quality assurance activities to ensure minimal defects. This free and open-source operating system has claims of robustness and quality [26]. Real-time and embedded software is found commonly in systems directly impacting human life and require a low defect rate. In such critical software, traditional quality assurance may not suffice in minimizing software defects. When traditional software quality assurance is not enough for defect removal, software engineering formal methods may help minimize defects. A formal method such as program verification is useful for proving correctness in real-time soft- ware. Microsoft Research created Dafny for proving program correctness. It contains a programming language with specification constructs. A program verification tool such as Dafny allows for proving correctness of FreeRTOS's modules. We propose using Dafny to verify the correctness of FreeRTOS' scheduler and supporting API.

Committee: Nigamanth Sridhar PhD (Committee Chair); Yongjian Fu PhD (Committee Member); Chansu Yu PhD (Committee Member) Subjects: Computer Science

MS, University of Cincinnati, 2001, Engineering : Computer Engineering

An active network describes a new generation of network where all network nodes are programmable. Nodes can be configured according to user requirements at booting or on-the-fly, and each node can also provide computational capabilities to process regular data carrying packets. The flexibility gained in the dynamics of active networks gives rise to significant security and safety issues. In this thesis, we apply Formal Methods to the specification of an active node. The specification process consists of designing a formal framework and then evaluating it. Constructive and axiomatic specifications are used during the design. Evaluation of the framework is achieved by building a working node model and verifying that the model demonstrates the critical properties of an active node. The formal framework and model are both written in the Prototype Verification System (PVS) language. The PVS theorem prover is then used for verifying and validating the proposed model.

Committee: Perry Alexander (Advisor) Subjects: Computer Science

PhD, University of Cincinnati, 2001, Engineering : Computer Science and Engineering

Hardware and software systems are becoming increasingly complex. To design systems of such high complexity, a fundamental shift in the design process is necessary. A more active application of formal analysis techniques will enable error detection during the preliminary states of design, thereby considerably reducing the cost of systems development. Formal analysis techniques also provide the rigor required for analyzing safety-critical systems. But the application of formal analysis techniques is a very specialized area. It is impractical to expect system designers to also have expertise in another specialized area. In this work, we present an automated approach to formally analyzing system designs for common categories of errors. This work proposes the use of proof obligations for the analysis of component-based hierarchical designs. More specifically, the focus of this work is on automating the process of identifying, generating and possibly verifying proof obligations for a given design. Though conceptually this approach could be applied to a model in anyrequirements specification language, for the purpose of illustrating the effectiveness of the approach, the VSPEC language has been used. A problem frequently faced when formally analyzing correctness of systems is identifying what needs to be proved. Moreover, when proving the correctness of the system as a whole, theorems can become complicated. We have identified certain necessary conditions that need to be satisfied by all designs with a certain architecture. We make use of the architecture inherent in the design to simplify the theorems. The VSPEC specifications are automatically translated into corresponding models in PVS. The details of interconnections among the components, obtained from VSPEC architectures, are used in conjunction with the identified rules to generate the proof obligations. These obligations are inserted as theorems into the generated PVS theories. The PVS verifier is used to attempt a (open full item for complete abstract)

Committee: Dr. Perry Alexander (Advisor) Subjects:

MS, University of Cincinnati, 2002, Engineering : Computer Engineering

The essence of systems engineering is the ability to aggregate heterogeneous information into design decision making processes. The Systems Level Design Language (SLDL) community is currently examining solutions to the problems presented by a heterogeneous modeling language.One such modeling language is Rosetta developed under the aegis of the SLDL forum. To facilitate the use of Rosetta within the system level design community, tools like parsers, theorem provers, model checkers etc. are necessary. The main thrust of this work is towards the development and implementation of a type checking algorithm to facilitate semantic checking in the Rosetta parser. In particular, this work focuses on handling scenarios that present incomplete type information during type checking. For a conventional programming language such cases are explicit semantic errors as their sole purpose is code generation - and code generation almost always needs complete type resolution (except for languages that support dynamic typing). However, for modeling languages that use higher levels of abstraction such type details may not always be specified or available. The solution then is to generate Type-Safety Obligations (TSOs) that need to be proven within the context of the specification being parsed if the specification is to be deemed semantically correct. In this thesis we discuss the motivation and the semantic basis of TSOs. We also identify the different cases where TSOs can be generated and the resulting TSO for each such case. To demonstrate the feasibility of the ideas developed, we also present an example specification and the resulting TSOs that are generated by the Rosetta parser.

Committee: Perry Alexander (Advisor) Subjects:

Master of Science, The Ohio State University, 2012, Computer Science and Engineering

Formal specifications are widely recognized as beneficial, and in some niches, formal methods have been gaining ground. Unfortunately, many legacy systems have no formal specification -- this is the ``legacy code problem''. Many such systems could benefit from additional specifications -- such specifications can serve as useful documentation, acting as educational tools for new users and aides to maintaining system integrity as the system is modified over its lifecycle. Even though training for and acceptance of formal methods is increasing, the sheer amount of unspecified legacy code is daunting. Clearly any assistance, automated or semi-automated, would be of considerable value. Along a different route, automated testing and related techniques such as test-driven development are now recognized as a good practice in industry, and many systems have robust test suites for exercising a majority of their code base. Dynamic analysis systems such as Daikon and DIDUCE can take advantage of such test suites to infer specifications for systems under analysis, but they show sensitivity to the values of test inputs, possibly inferring incorrect invariants based on those values. One possible mitigation approach is to allow hand-written specifications, thereby overriding incorrect or extraneous inference, but the above systems do not support such a technique. The work reported in this thesis is based on the idea that, by starting with a body of pre-specified core methods (rather than relying on statistical confidence metrics as with systems such as Daikon), an automated system may be able to arrive at better specifications. How can we build upon such a foundation? Interestingly, similar questions have been raised in type research. Rubydust approaches the issue of inferring static types for the dynamically typed Ruby language. Utilizing observations recorded during test runs, it employs a constraint-based dynamic analysis approach that builds upon given specifications of core R (open full item for complete abstract)

Committee: Neelam Soundarajan PhD (Advisor); Bruce Weide PhD (Committee Member) Subjects: Computer Science

Master of Computer Science, Miami University, 2009, Computer Science and Systems Analysis

Formal specification languages can be used to support the rigorous development of complex software systems when these systems must be of high quality. Unfortunately, writing formal specifications and refining them into designs can be a challenging activity. Use of design patterns, which are a widely accepted design activity, helps create quality designs, but adds further complexity to the design activity.We have developed a tool ADEPT, Advanced Design Employing Pattern Templates, that aids designers in using both formal specifications and design patterns. The software developer will use the ADEPT tool to guide them through the process of choosing a design pattern that is related to their formal system specification for the purpose of automatically supporting refinement. The user is guided through refining the specification and creating a design that not only incorporates one of the design patterns but also meets the given system specification.

Committee: Ann Sobel PhD (Advisor); James Kiper PhD (Committee Member); Gerald Gannod PhD (Committee Member) Subjects: Computer Science