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

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, 2018, Computer Science and Engineering

Performance has been the focus of computer systems for decades, from past Moore law to current parallel computers. Compiler optimizations are used to improve performance by generating code to utilize hardware (e.g. cache)component efficiently. However, modern systems such as large scale system require not only performance but also resilience and energy efficiency. Increasing concern of system resilience and energy efficiency has been shown in both industry and academia. Errors within applications, especially those escape from detection and resulting in silent data corruption, are extremely problematic. Thus, in order to improve the resilience of applications, error detection and vulnerability characterization techniques are an important step towards fault tolerant applications. Compiler transformations, which restructure programs to improve performance by leveraging data locality and parallelism, are often complex and possibly involve bugs that leads to errors in transformed programs. Thus it is essential to guarantee the correctness, however, current approaches suffers from various problems such as transformations supported or space complexity etc. This dissertation presents a novel approach that performs dynamic verification by inserting lightweight checker codes to detect errors of transformations. The errors are exposed by the execution of checker-inserted transformed program if exist. Energy efficiency is of increasingly importance in scenarios ranging from battery-operated devices to data centers striving for lower energy costs. Dynamic voltage and frequency scaling (DVFS) adapts CPU power consumption by modifying processor frequency to improve energy efficiency. Typical DVFS approaches involve default strategies such as reacting to the CPU runtime load to adapt frequency, which have inherent limitations because of processor-specific and application-specific effects. This dissertation developed a novel compile-time characterization to select frequency (open full item for complete abstract)

Committee: Ponnuswamy Sadayappan (Advisor); Gagan Agrawal (Committee Member); Radu Teodorescu (Committee Member); Louis-Noel Pouchet (Committee Member); Sriram Krishnamoorthy (Committee Member) Subjects: Computer Science

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

For a variety of reasons, software must evolve to cope with change. Unfortunately, evolution and maintenance is an expensive, time-consuming, and error-prone task, especially when the system in question is large and complex. Typically, a change to a single program element requires changes to related, and often seemingly unrelated, elements scattered throughout the source code. To address this problem, approaches have emerged to mechanically assist developers with a wide range of software evolution and maintenance tasks. This assistance is typically provided in the form of extensions (plug-ins) to integrated development environments (IDEs) that afford (semi-) automated aid in carrying out these tasks, thus easing the burden associated with evolution and maintenance. Although existing approaches are useful in alleviating some of the burden associated with software evolution and maintenance, there are a number of situations where developers are still required to complete evolution and maintenance tasks manually. Automated approaches to assist developers with such cumbersome and error-prone tasks would be extremely useful in evolving and maintaining large, complex systems. In this thesis, I develop several new techniques that can be of great value to software developers in evolving code to accommodate change. The first is an automated refactoring that upgrades legacy Java code to use proper language enumeration (enum) types, a feature of the modern Java language. I have developed an approach that preserves semantics and that allows us to migrate legacy applications by automatically replacing a predominantly used pattern with suitable use of enums. The second technique is an automated approach to assist developers in maintaining pointcuts in evolving Aspect-Oriented (AO) programs. AO languages enable developers to better encapsulate crosscutting concern (CCC) implementations by allowing them to create an expression (a pointcut) which specifies well-defined points ( (open full item for complete abstract)

Committee: Neelam Soundarajan PhD (Advisor); Atanas Rountev PhD (Committee Member); Paul A. G. Sivilotti PhD (Committee Member); Paul Evans PhD (Committee Member) Subjects: Computer Science