In line with Augusta University's mission to become a top-tier research institution, School of Computer and Cyber Sciences faculty members are conducting research to stay one step ahead of today's ever-changing, technology-driven society. Research opportunities are available for our students as well, giving them additional experience in this field.
Student Research Assistants (from left) Nick Wylds, Thomas Gordon and Eric Kilgore analyze security of medical devices in the Georgia Cyber Center.
Dr. Clement Aubert: Implicitly Restricting Programming Languages
Over-consumption of resources (memory, CPU) by a program can cause it to crash, and offers many vulnerabilities to external attack (exhaustion of resources, buffer overflow). Implicit Computational Complexity (ICC) uses mathematics (recursion theory, proof theory, model theory, Geometry of Interaction,) to define programming language enforcing resource bounds on the programs. A mathematical certificate guarantees that the programs will use only pre-allocated resources no matter the size of the input or the complexity of the tasks currently running. To-date, ICC has produced a theoretical understanding of bounded languages, designed proof of concepts, but has not yet been applied to design or restrict "real-world" programing languages. Our project is to use cutting-edge ICC research to design resource-aware programming languages.
Dr. Bogdan Chlebus: Adversarial Broadcasting on Shared Channels
This research presents distributed deterministic broadcast algorithms for multiple access channels when dynamic traffic is constrained by adversarial models. The communication network consists of stations attached to a shared channel. A message transmitted in a round is heard successfully by all the active stations only when exactly one station transmits. An adversary is restricted by a packet-injection rate and by how many packets can be injected in one round. Deterministic communication algorithms executed against such adversaries can have their performance assessed in the sense of worst-case bounds. Performance of algorithms is measured with respect to queue size and packet latency.
Dr. Harley Eades: From Attack Trees to Petri Nets
Cybersecurity professionals often use attack trees to visualize the various possible paths of attack on a resource. Such visualizations provide important tools for communication and threat analysis. However, they can quickly become complex and unwieldy, and must rely on humans for error-checking and the tracing of possible paths. We are working to translate attack trees into Petri nets, mathematical graphical models that can be analyzed and verified much more quickly and accurately. In their original form, Petri nets are constructed of places and transitions between places, with a flow relation indicating how resources can flow through the net, or what sequence of steps is needed to get from one point to another in the net. We have begun development of a chainable Petri net, which facilitates the construction of complex nets using simple logical operations already found in attack trees. Once constructed, these nets can be analyzed using the powerful tools native to the Petri net model. This will enable cybersecurity professionals to check two nets for equivalence or hierarchy, incorporate one net into another, compute possibilities under given circumstances, and complete many other tasks with greater speed and accuracy than is possible under the current model.
Formal Methods
The ForML (Formal Methods and Computational Logic) Lab in the School of Computer and Cyber Sciences at Augusta University strives to advance the software development process by utilizing the principles and techniques from logic, mathematics, and interactive/automated theorem proving to ensure the correctness of software. The primary research areas of the faculty and students in the ForML lab are: foundations of programming languages, interactive theorem proving, categorical logic, reversible computing, and secure programming. Dr. Paul Attie, Dr. Eades and Dr. Clement Aubert are collaborating on this research topic.
Programming Language Development
The Granule Project is an ambitious research project whose goal is to rethink the foundations of statically-typed functional programming languages by making resource sensitivity an integral aspect of the language design. Our work strives to show that by combining a linear type system with fine-grained (co)effects via graded modal types one obtains a very powerful programming language capable of precisely enforcing resource usage throughout the language. We are actively developing a prototype implementation called Granule based on our research. In addition, we are developing a new dependent type theory that will greatly expand the expressive power of Granule’s type system.
Dr. Michael Nowatkowski: Medical Device Security
The initial goal of the research is to generate knowledge about device interactions with the environment. Dr. Nowatkowski's longer-term goal is to make recommendations for the design of more secure devices. Several examples of researchers finding Medical and Health Monitoring Devices (MHMD) vulnerabilities exist, including on infusion pumps (Zetter 2015; ICS-CERT 2015), pacemakers (Seals 2017; FDA Safety Communication 2017), and insulin pumps (Finkle 2016; ICS-CERT 2016). Through experimentation with MHMDs, investigators will look for common security flaws in the communications, such as plain text username/password pairs, and plain text data. The investigators will also apply hardware reverse engineering tools to examine the security of physical access methods. Other experiments will be conducted referencing the FDA’s guidance for pre-market and post-market assessments of MHMDs (Food and Drug Administration 2014, 2016).
Dr. Alex Schwarzmann: Distributed Computing
This research investigates computability, algorithmics, and complexity in distributed settings where a collection of machines cooperate on solving computation problems in the presence of dynamic changes in the computing medium. The computation problems are modeled as collections of tasks, such as the problems frequently occurring in the Internet supercomputing. This research aims to develop efficient algorithms with rigorously proved correctness, efficiency and fault-tolerance guarantees. The investigation includes the associated resource discovery problem of identifying the nodes in the distributed system that are willing and able to cooperate. This research also studies supporting services that can provide effective implementations of communication and shared-memory primitives in target dynamic platforms. In particular, a major direction here is to develop distributed implementations of data sharing services that provide rigorous consistency guarantees (atomicity/linearizability) while tolerating failures. An important goal here is to provide algorithms that are efficient both in terms of local computation and in terms of communication latency.
Dr. Weiming Xiang: Safety Verification for Learning Enabled Cyber Physical Systems
The ongoing renaissance in artificial intelligence (AI) has led to the advent of machine learning methods deployed within components for sensing, actuation, and control in safety-critical cyber-physical systems (CPS), and is enabling autonomy in such systems, such as autonomous vehicles and swarm robots. However, as demonstrated in part through recent accidents in semi-autonomous/autonomous CPS and by adversarial machine learning, ensuring such component operate reliably in all scenarios is extraordinarily challenging. In our recent work as part of the ongoing DARPA Assured Autonomy project “Assurance-Based Learning-Enabled Cyber-Physical Systems (ALC)”, we have developed a safety verification framework for CPS equipped with neural network components. Dr. Xiang's research discusses and clarifies that the key for safety verification of neural-network-based CPS is the reachable set computation for neural networks. This research also looks into two major methods developed for reachable set computation of feedforward neural networks. Then combining the two methods with state-of-the-art tools for hybrid system reachability, this research accomplishes the safety verification for learning enabled CPS with neural network components, which will be demonstrated by a spring-electromagnet system example and an adaptive cruise control (ACC) system case study.
Dr. Paul York: Natural Interfaces to Computing in Healthcare (NICHe)
This interdisciplinary research stream focuses on the utilization of modern computing modalities to reduce costs and improve healthcare outcomes. “Natural interfaces” encompass most any non-traditional method of interacting with computing resources, including touch, voice, motion capture, haptics, and wearables as well virtual and augmented reality. The main areas of focus are increasing the efficiency and effectiveness of healthcare workers and enabling better remote, in-home healthcare. The first research project in this stream is a telerehabilitation system dubbed a System for Technology Augmented Rehabilitation and Training (START). In partnership with researchers in AU’s Neurology and Physical Therapy departments, this grant-funded project has embedded a custom designed motion capture system into the homes of individuals with Parkinson’s Disease with the goal of encouraging and improving the efficacy of prescribed, self-directed exercise regimens. Additional projects are ongoing.
