Category: CS

ROTC Cybersecurity Training for Tomorrow’s Officers

The U.S. Department of Defense, Office of Naval Research, has awarded Michigan Tech faculty researchers a $249,000 grant that supports the creation of an ROTC undergraduate science and engineering research program at Michigan Tech. The primary goal of the program is to supply prepared cadets to all military branches to serve as officers in Cyber commands.

The principal investigator (PI) of the project is Andrew Barnard, Mechanical Engineering-Engineering Mechanics. Co-PIs are Timothy Havens, College of Computing; Laura Brown , Computer Science, and Yu Cai, Applied Computing. The title of the project is, “Defending the Nation’s Digital Frontier: Cybersecurity Training for Tomorrow’s Officers.”

The curriculum will be developed over the summer, and instruction associated with the award will begin in the fall 2020 semester. Cadets interested in joining the new program are urged to contact Andrew Barnard.

Initially, the program will focus on topics in cybersecurity, machine learning and artificial intelligence, data science, and remote sensing systems, all critical to the The Naval Science and Technology (S&T) Strategic Plan and the Navy’s Force of the Future, and with equal relevance in all branches of the armed forces.

The plan of work focuses on on engaging ROTC students in current and on-going Cyber research, and supports recruitment of young ROTC engineers and scientists to serve in Navy cybersecurity and cyber-systems commands. The program will compel cadets to seek positions within Cyber commands upon graduation, or pursue graduate research in Cyber fields.

“Our approach develops paid, research-based instruction for ROTC students through the existing Michigan Tech Strategic Education Naval Systems Experiences (SENSE) program,” said principal investigator Andrew Barnard, “ROTC students will receive one academic year of instruction in four Cyber domains: cybersecurity, machine learning and artificial intelligence (ML/AI), data science, and remote sensing systems.”

Barnard says the cohort-based program will enrich student learning through deep shared research experiences. He says the program will be designed with flexibility and agility in mind to quickly adapt to new and emerging Navy science and technology needs in the Cyber domain. 

Placement of officers in Cyber commands is of critical long-term importance to the Navy (and other DoD branches) in maintaining technological superiority, says the award abstract, noting that technological superiority directly influences the capability and safety of the warfighter.

Also closely involved in the project are Michigan Tech Air Force and Army ROTC officers Lt. Col. John O’Kane and LTC Christian Thompson, respectively.

“Unfortunately, many ROTC cadets are either unaware of Cyber related careers, or are unprepared for problems facing Cyber officers,” said Lt. Col. O’Kane. “This proposal aims to provide a steady flow of highly motivated and trained uniformed officers to the armed-services, capable of supporting the warfighter on day-one.”

Andrew Barnard is director of Michigan Tech’s Great Lakes Research Center, an associate professor of Mechanical Engineering-Engineering Mechanics, and faculty advisor to the SENSE Enterprise.

Tim Havens is director of the Institute of Computing and Cybersystems, associate dean for research, College of Computing, and the William and Gloria Jackson Associate Professor of Computer Systems.

Laura Brown is an associate professor, Computer Science, director of the Data Science graduate program, and a member of the ICC’s Center for Data Sciences.

Yu Cai is a professor of Applied Computing, an affiliated professor of Computational Science and Engineering, a member of the ICC’s Center for Cybersecurity, and faculty advisor for the Red Team, which competes in the National Cyber League (NCL).

The Great Lakes Research Center (GLRC) provides state-of-the-art laboratories to support research on a broad array of topics. Faculty members from many departments across Michigan Technological University’s campus collaborate on interdisciplinary research, ranging from air–water interactions to biogeochemistry to food web relationships.

The Army and Air Force have active ROTC programs on Michigan Tech’s campus.

The Office of Naval Research (ONR) coordinates, executes, and promotes the science and technology programs of the United States Navy and Marine Corps.


Ali Ebnenasir is Co-author of Article in ACM Transactions on Computational Logic

Ali EbnenasirAli Ebnenasir (SAS/CS), professor of computer science, is co-author of the article, “On the verification of livelock-freedom and self-stabilization on parameterized rings,” published in the July 2019 issue of the journal ACM Transactions on Computational Logic. The article is co-authored by Alex Klinkhamer of Google.

Abstract: This article investigates the verification of livelock-freedom and self-stabilization on parameterized rings consisting of symmetric, constant space, deterministic, and self-disabling processes. The results of this article have a significant impact on several fields, including scalable distributed systems, resilient and self-* systems, and verification of parameterized systems. First, we identify necessary and sufficient local conditions for the existence of global livelocks in parameterized unidirectional rings with unbounded (but finite) number of processes under the interleaving semantics. Using a reduction from the periodic domino problem, we show that, in general, verifying livelock-freedom of parameterized unidirectional rings is undecidable (specifically, Π10-complete) even for constant space, deterministic, and self-disabling processes. This result implies that verifying self-stabilization for parameterized rings of self-disabling processes is also undecidable. We also show that verifying livelock-freedom and self-stabilization remain undecidable under (1) synchronous execution semantics, (2) the FIFO consistency model, and (3) any scheduling policy. We then present a new scope-based method for detecting and constructing livelocks in parameterized rings. The proposed semi-algorithm behind our scope-based verification is based on a novel paradigm for the detection of livelocks that totally circumvents state space exploration. Our experimental results on an implementation of the proposed semi-algorithm are very promising as we have found livelocks in parameterized rings in a few microseconds on a regular laptop. The results of this article have significant implications for scalable distributed systems with cyclic topologies.

Citation: Klinkhamer, A., & Ebnenasir, A. (2019). On the verification of livelock-freedom and self-stabilization on parameterized rings. ACM Transactions on Computational Logic, 20(3), 16:1-16:36. http://dx.doi.org/10.1145/3326456

MTU Digital Commons link: https://digitalcommons.mtu.edu/michigantech-p/146/

ACM link: https://dl.acm.org/citation.cfm?doid=3338853.3326456


Ali Ebnenasir is Co-Author of Publication in ACM Transactions on Computational Logic

Ali Ebnenasir

An article co-authored by Ali Ebnenasir (SAS/CS) and Alex Klinkhamer, “Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings,” was recently published in ACM Transactions on Computational Logic.

Abstract: This article investigates the verification of livelock-freedom and self-stabilization on parameterized rings consisting of symmetric, constant space, deterministic, and self-disabling processes. The results of this article have a significant impact on several fields, including scalable distributed systems, resilient and self-* systems, and verification of parameterized systems. First, we identify necessary and sufficient local conditions for the existence of global livelocks in parameterized unidirectional rings with unbounded (but finite) number of processes under the interleaving semantics. Using a reduction from the periodic domino problem, we show that, in general, verifying livelock-freedom of parameterized unidirectional rings is undecidable (specifically, Π10-complete) even for constant space, deterministic, and self-disabling processes. This result implies that verifying self-stabilization for parameterized rings of self-disabling processes is also undecidable. We also show that verifying livelock-freedom and self-stabilization remain undecidable under (1) synchronous execution semantics, (2) the FIFO consistency model, and (3) any scheduling policy. We then present a new scope-based method for detecting and constructing livelocks in parameterized rings. The proposed semi-algorithm behind our scope-based verification is based on a novel paradigm for the detection of livelocks that totally circumvents state space exploration. Our experimental results on an implementation of the proposed semi-algorithm are very promising as we have found livelocks in parameterized rings in a few microseconds on a regular laptop. The results of this article have significant implications for scalable distributed systems with cyclic topologies.

https://dl.acm.org/citation.cfm?id=3326456&dl=ACM&coll=DL

doi: 10.1145/3326456


Soner Onder To Present Invited Talk

Soner OnderDr. Soner Onder (CS, SAS) will present an invited talk titled “Program semantics meets architecture: What if we did not have branches?” at a workshop organized in honor of the 80th birthday of Prof. Yale Patt of University of Texas, Austin. Prof. Patt is a prominent researcher with decades of accomplishments in Computer Architecture.

The workshop, titled “Yale:80 in 2019, Pushing the Envelope of Computing for the Future,” will take place July 1-2, 2019, in Barcelona, Spain. The workshop is organized by Universitat Politècnica de Catalunya and Barcelona Supercomputing Center, and sponsored by the Ministry of Science, Innovation and Universities of Spain, among others.