Project Detail


With the complexity increasement and constant exposure to unknown environments in todays’ cyberspace, it is becoming more and more challenging to build trusted and attack resilient military computing systems. Therefore, one of the major goals of DOD information innovation is to build trusted, adaptive, attack-resilient cyber physical systems. The ultimate goal of this project is to develop a light-weight formal methodology and tools to facilitate the development of attack resilient cyber physical systems that are able to dynamically adapt to a constantly evolving environment.

Formal methods have been adopted to ensure trustworthiness with high confidence in the past years. Model checking, theorem proving, and static analysis are the typical formal approaches to ensuring trusted and high assurance software intensive and resilient systems. However, these approaches all have drawbacks. Model checking suffers the state space explosion problem, especially in the presence of concurrency and unbounded types. Although many heuristic methods have been developed, such as abstraction, and partial-order reduction, scalability is still an issue when model checking large scale systems.

In contrast, runtime verification provides a complementary, dynamic and scalable validation technique for large software intensive systems. Runtime verification combines the advantages of formal methods and software testing – trusted aspects are formally specified and functionality checking is realized through monitoring checking points during program execution. In addition, performance overhead is very limited because the use of aspect-oriented programming for program instrumentation.

Detecting and identifying a hostile attack correctly is only the first step for attack resilient systems to adapt their behavior. The more important task is to explore all candidate possibilities to find the best adaptation solution in a timely manner so that cyber physical systems can continue to accomplish their missions without compromising security. Rigid approaches do not support the dynamic adaptation to changes caused by malicious attacks and exploits. Evolutionary algorithms (EA) are more suitable to make the best selection among the possible execution traces for multiple components and subsystems; and are particularly effective at producing solutions to problems with a large searching space. The objective of this work is to develop a novel approach to ensuring high confidence, trusted and attack-resilient software intensive systems by synthesizing the runtime verification with a hierarchical evolutionary algorithm (HEA), an improved version of traditional evolutionary algorithms. This method is investigated in both design and implementation level. To validate the methodology, a cyber physical system (CPS) (Proof-of-Concept System) Java program will be developed to cover benign and malice requirements in both model and implementation levels. The security policies will be defined at design or implementation level. When a security property/policy is violated, the evolution model finds a solution based on HEA to handle and recover from hostile attacks so that the cyber physical system can continue to fulfill its predefined missions.


Research Thrust


This project was funded in Dec 2014, and started at March 2015. The project includes four research components – modeling, runtime verification, information flow security, and proof of concept platform. The combination these four research component will generate an adaptive runtime checker to discover z-day attack and repair the system to ensure mission completion.


News


  • Oct 16-18, 2015 -- project YR1 kick off meeting
  • Nov 3-5, 2016 – project YR2 kick off meeting
  • Jul 10-13, 2017 – project YR3 kick off meeting

Publications


  [1] Xudong He, Zhijiang Dong, Heng Yin and Yujian Fu, “A Framework for Developing Cyber Physical Systems”. International Conference of Software Engineering and Knowledge Engineering, 2017

  [2] Yujian Fu, Xudong He, and Zhijiang Dong, “An Agent Oriented Framework of Multiple Robotics Systems”. International Journal of Robotics and Applications, 2017.


Participant & Training


Enhancing Research Experience For Graduate Students in Runtime Verification on CPS System (eREGS-RV-CPS)

An Overview

This program is created to enhance Research Experiences for graduate students (eREGS) at the runtime verification on CPS systems. The program is open to up to 3 graduate students from across the U.S. and planned for 3 months to 12 month. Undergraduate students with highly motivation in research are also welcome. The purpose of this eREGS is to engage graduate/undergraduate students in the runtime verification on multiple disciplinary research and inspire them for graduate and research careers. Funding (participant stipend plus additional benefits) is provided from Air Force Research Lab. Women, veterans, and underrepresented minorities are especially encouraged to apply.

The Research Theme

The main theme of this opportunity is in the application of Runtime Verification in general area of Mobile Cyber-Physical Systems. A Mobile CPS refers to a system composed of physical and computation components that are mobile and can communicate over a network. A swarm of robots is an example of a Mobile CPS. Users roaming with their cell phones is another example of a mobile CPS. Here are few example applications:

  • Object recognition, localization, and avoidance
  • Trajectory generation, map generation
  • Target tracking, search and
  • Sophiscated task completion, e.g., rescue and patrol control
  • Intelligent transportation systems and vehicular networks
  • Sensing with mobile nodes

This program is renewable with performance evaluation on each research component. This eREGS will focus on the following broad areas of mobile CPSs:

  • Formal Modeling and Verification analysis of cyber-physical interactions
  • Runtime Verification
  • Mobile devices and embedded software platforms
  • Mobile cyber-physical applications and services
  • Wireless networking and mobile communication
  • Firmware security for embedded devices
  • Wireless security in vehicular networks and robotics

The projects will be conducted in our Formal Methods on CPS Lab that is equipped with various robots (e.g., IRIS+ and NAO H-12, H-25, Bioloid (GP/Premium), Arduino ) and sensors (e.g., DMS sensors).

The Setup

Each student will work closely with one of the faculty mentors on a specific research project for the duration of the program. Weekly meetings will bring all the students and mentors together to exchange ideas and ensure progress. Monthly project presentation will ensure the project progress with schedule. Various activities are planned throughout the summer session (e.g., tutorials, seminars, industry visits, picnics, etc...).


Program Application

This program is created to enhance Research Experiences for graduate students (eREGS) at the runtime verification on CPS systems. The program is open to up to 3 graduate students from across the U.S. and planned for 3 months to 12 month. Undergraduate students with highly motivation in research are also welcome. The purpose of this eREGS is to engage graduate/undergraduate students in the runtime verification on multiple disciplinary research and inspire them for graduate and research careers. Funding (participant stipend plus additional benefits) is provided from Air Force Research Lab. Women, veterans, and underrepresented minorities are especially encouraged to apply.

Timeline

You will be required to complete minimum 3 month activities once your application is accepted. Your participant term will be from 3 months to 12 months depends on the initial participant contract of your applied research component.

Application Process:

STEP 1: As an applicant, you will be asked to complete the application package (following instruction on the web site) in consideration of your candidacy for the eREGS program.

STEP 2: Upon completion of this application, you will be forward this application package directly back to the web page.

STEP 3: At the web page, you will be directed to submit any additional materials that are requested as part of the institutional application.

Additional Materials:

  1. One/Two letters of recommendation.
  2. A copy of your current academic transcript, mailed separately.

Mail all materials to: yujian.fu@yahoo.com

STEP 4: Notification of acceptance information will be mailed to the applicants.

Eligibility

Applicants must be a current registered graduate or undergraduate student in good standing; plan to complete an graduate or undergraduate degree program, and may include high school students who have been accepted at the university hosting the site to which they are applying.High school graduates who have been accepted at an undergraduate institution but who have not yet started their undergraduate study are also eligible to participate.

Contact Information

Dr. Yujian Fu Alabama A&M University Department of EE&CS, AL 35762 yujian.fu@yahoo.com 256-372-8461


Team


Faculty: Dr. Yujian Fu, AAMU