Research

Dr. Paul Attie: Distributed Computing Modeling

This research addresses the conceptual difficulty and the computational complexity of the design and verification of large concurrent software systems. Dr. Attie has produced models and results for complex dynamic behavior (Dynamic Input-output Automata), deadlock freedom, fault-tolerance (impossibility of boosting fault-tolerance) and for reducing the complexity of reasoning about finite-state concurrent programs (pairwise normal form and software architectures). By representing a finite-state concurrent program in pairwise normal form, Dr. Attie produced algorithms for tractable (polynomial time) checking of deadlock-freedom, safety, and liveness of finite-state concurrent programs. Software architectures enforce correctness properties by applying coordinators to a concurrent program, so post hoc verification is not necessary. Dr. Attie has devised a method for the automatic repair of a finite Kripke structure so that it satisfies a given CTL formula, and have implemented this method in the Eshmun tool. By extending the repair method to pairwise normal form, Eshmun is capable of repairing state-spaces of up to 3^50 states. Repair can also be applied to concurrent programs by simulating the program to generate its Kripke structure, repairing the structure, and then extrating a correct program from the repaired structure.

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. Dariusz Kowalski: Classic Distributed and Parallel Algorithms

Dr. Kowalski has studied classical problems in (algorithmic) distributed and parallel computing for more than 20 years. The study includes fundamental models (message-passing, shared memory, shared channel), problems (consensus/agreement, mutual exclusion, leader election, information spreading/gathering, performing work, reading/writing to shared registers) and settings (synchrony and asynchrony, Byzantine and crash/omission failures, static and dynamic input). Efficiency of algorithms has been analyzed in terms of number of steps, number and size of messages, number of operations (e.g., reads/writes). The main line of results show how the setting features influence the performance of the system. The current project concentrate on further improvements on consensus and renaming problems.

Communication in Wireless Networks

The second important area of Dr. Kowalski's algorithmic research addresses various aspects of communication in wireless networks, including: distributed and centralized communication, online and offline algorithms, several types of performance measures and their combinations/trade-offs (such as latency, throughput, stability, energy), various types of models (collision-free, radio networks, SINR model), worst-case and stochastic measurements, game-theoretical aspects. The list of communication problems includes: routing, multi-broadcasting, local broadcast and link scheduling, contention resolution, wake-up, leader election. They have been studied from perspective of how specific features (e.g., model parameters, class of algorithms, performance constraints) influence feasibility and performance of optimal solution, both upper bounds (achieved by algorithms) and lower limits. Important properties such as fairness and stability were also analyzed. Current research problems include generalization of the SINR model to more realistic setting, and study of complex tasks such as dynamic routing or link scheduling.

Dr. Hoda Maleki: Application of the Universal Composition Framework to the Security Analysis of Complex Hardware Systems

Modern hardware typically is characterized by a multitude of interacting physical components and software mechanisms. In order to rigorously analyze (and prove) its security, we need to understand accurately how the security guarantees of its individual parts compose and inherit themselves within the main system. This can be a non-trivial task. A structurally similar framework, in which arbitrarily interleaving cryptographic protocols can be studied and formally proven secure, is long known within theoretical cryptography: The so-called Universal Composition (UC) framework. Transferring its sophisticated toolbox to a hardware context promises new, provable results on the feasibility and infeasibility of secure hardware composition. This work takes the first steps in this direction and hopes to open up a new research avenue along these lines. In this project, we are investigating in detail to what extent the UC framework can be utilized in the analysis of complex hardware, and how its toolbox can facilitate a novel type of modular hardware security analysis. 

Encrypted Search System

In a typical message system, including most chat networks and emails, messages are only encrypted between the sender and the application service provider, and between the application service provider and the receiver. This means that the application service provider is able to read the messages, which allows it to provide features such as scan for illegal or unacceptable content. However, in the end-to-end encryption application, only the sender and the receiver of the message are able to read the content. Recently, attackers are taking advantage of this end-to-end encryption feature to secretly spread rumors and false news, preventing the application service provider from detecting or flagging the suspicious content.  These rumors have led to violence, for example lynchings in India incited by false stories spread over WhatsApp.

The aim of this project is to enable the detection and later prevent the spread of these false messages. To this extent, we would like to design an encrypted search system for end-to-end systems that allows the server to (possibly obliviously) flag the suspicious messages while preserving the normal security features of end-to-end encrypted chat: privacy of non-malicious messages, authenticity, deniability, and forward secrecy.

Privacy-Preserving Smart Contract

Ethereum is a blockchain-based distributed computing platform that can be used to build smart contracts and decentralized applications. Smart contracts are self-executing contracts that automatically execute when predetermined conditions are met. The Ethereum platform has become popular as a way to remove the need of the third party trust and add transparency to distributed applications. However, Ethereum by itself does not provide privacy, i.e., all calculations and transactions are publicly visible. In this project, our aim to introduce practical privacy-preserving smart contracts that can be implemented in the current Ethereum platform.

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.