Digital Library

Authors: Sagar Chaki, James Edmondson

In this podcast, James Edmondson and Sagar Chaki describe an architecture and approach to engineering high-assurance software for Distributed Adaptive Real-Time (DART) systems.

Authors: Sagar Chaki

Watch Sagar Chaki in this SEI Cyber Minute as he discusses "Assuring Autonomous Software".

Topics: Software Assurance

Authors: Sagar Chaki, Dionisio de Niz

This paper presents two challenge problems guiding research on developing a provably correct approach for runtime assurance of distributed real-time embedded systems.

Topics: Cyber-Physical Systems

Authors: Björn Anderson, Sagar Chaki, Dionisio de Niz, Jeffrey Hansen, Scott Hissam, John J. Hudak, Mark H. Klein, David Kyle, Gabriel Moreno

Cyber-physical systems (CPS) integrate computational algorithms and physical components. SEI promotes efficient development of high-confidence, distributed CPS.

Topics: Process Improvement

Authors: Sagar Chaki, Scott Hissam, Gabriel Moreno, Linda M. Northrop, Kurt C. Wallnau

Predictability by construction (PBC) makes the behavior of a component-based system predictable before implementation, based on known properties of components.

Authors: Sagar Chaki, Dionisio de Niz

This work is producing validated assurance techniques for distributed adaptive real-time (DART) systems

Authors: Sagar Chaki, Dionisio de Niz

Software that accesses the system clock is the key to real-time and cyber-physical systems

Authors: Sagar Chaki

Formally verify STACs at the source code level using deductive (aka auto-active) verification

Authors: Sagar Chaki

DART Vision

Authors: Sagar Chaki, Dionisio de Niz

In this paper, the authors focus on proving the correctness of the budget enforcement that guarantees that no task τi executes beyond its W1 i. They present their approach and some preliminary results.

Topics: Cyber-Physical Systems

Authors: Sagar Chaki, Dionisio de Niz, Joe Seibel

This paper provides an end-to-end framework where DART systems can be designed, analyzed, and implemented within the same toolchain. In this talk, the authors present this toolchain and demonstrate it on a few representative examples.

Authors: Stanley Bak (Air Force Resarch Laboratory), Sagar Chaki

This work proposes a bridge between two important verification methods, software model checking and hybrid systems reachability.

Authors: Jeffrey Hansen, Sagar Chaki, Scott Hissam, James Edmondson, Gabriel Moreno, David Kyle

In this conference paper, the authors describe an approach to Statistical Model Checking (SMC). This paper is part of the Lecture Notes in Computer Science book series.

Topics: Cyber-Physical Systems

Authors: Sagar Chaki, David Kyle

DMPL is a language for programming distributed real-time, mixed-criticality software. It supports distributed systems in which each node executes a set of periodic real-time threads that are scheduled by priority and criticality.

Authors: Sagar Chaki, Derrick Karimi

This paper presents three variants of multi-threaded IC3s for model checking hardware, differing by degree of synchronization and aggressiveness of proof checking.

Authors: Mark H. Klein, Sagar Chaki, Dionisio de Niz

This presentation describes an evidence-based approach for producing high-assurance DART software involving multiple layers of the CPS stack.

Authors: Sagar Chaki, Dionisio de Niz

This poster describes the authors' research efforts in verifying distributed adaptive real-time systems.

Authors: Sagar Chaki, Dionisio de Niz

This 2015 Research Review presentation describes the authors' research efforts in verifying distributed adaptive real-time systems.

Authors: Sagar Chaki

In this 2015 Research Review presentation, the author describes his research efforts into scaling up software model checking—a fundamental challenge in the field.

Authors: Scott Hissam, Sagar Chaki, Gabriel Moreno

This short paper introduces our architecture and approach to engineering a DART system so that we achieve high assurance in its runtime behavior against a set of formally specified requirements.

Topics: Malware Analysis

Authors: Sagar Chaki, Cory Cohen, Arie Gurfinkel

In this article, the authors present a notion of similarity based on provenance; two binaries are similar if they are compiled from the same source code with the same compilers.

Topics: Malware Analysis

Authors: Wesley Jin, Sagar Chaki, Cory Cohen, Arie Gurfinkel, Jeff Havrilla, Chuck Hines, Priya Narasimhan (Carnegie Mellon University)

In this article, the authors present an alternative to pair wise comparisons based on "hashing” that captures the semantics of functions as semantic hashes.

Topics: Malware Analysis

Authors: Wesley Jin, Cory Cohen, Jeff Gennari, Chuck Hines, Sagar Chaki, Arie Gurfinkel, Jeff Havrilla, Priya Narasimhan (Carnegie Mellon University)

In this article, the authors present a static approach that uses symbolic execution and inter-procedural data flow analysis to discover object instances, data members, and methods of a common class.

Topics: Cyber-Physical Systems

Authors: Sagar Chaki, John M. Dolan, Joseph Giampapa

In this paper, the authors advocate, formalize, and empirically justify an approach to compute quantitative utility of robotic missions using probabilistic model checking.

Authors: Bjorn Andersson, Lori Flynn, David P. Gluch, Dennis Goldenson, Arie Gurfinkel, Jeff Havrilla, Chuck Hines, John J. Hudak, Carly L. Huth, Wesley Jin, Rick Kazman, Stephany Bellomo, Mary Ann Lapham, James McCurley, John McGregor, David McIntire, Robert Nord, Ipek Ozkaya, Brittany Phillips, Robert W. Stoddard, David Zubrow, Lisa Brownsword, Yuanfang Cai (Drexel University), Sagar Chaki, William R. Claycomb, Julie B. Cohen, Peter H. Feiler, Robert Ferguson

This report describes line-funded exploratory new starts (LENS) projects that were conducted during fiscal year 2012 (October 2011 through September 2012).

Authors: Sagar Chaki, Joseph Giampapa

This article introduces a reliability engineering assurance approach based on probabilistic model checking.

Authors: Len Bass, Rick Kazman, Edwin J. Morris, Brad Myers, William Nichols, Robert Nord, Ipek Ozkaya, Raghvinder Sangwan, Soumya Simanta, Ofer Strichman, Peppo Valetto, Nanette Brown, Gene Cahill, William Casey, Sagar Chaki, Cory Cohen, Dionisio de Niz, David French, Arie Gurfinkel

This report describes the line-funded exploratory new starts (LENS) projects that were undertaken during fiscal year 2011. For each project, the report presents a brief description and a recounting of the research that was done, as well as a synopsis of the results of the project.

Topics: Acquisition Support

Authors: Sagar Chaki, Rita C. Creel, Jeff Davenport, Mike Kinney (National Security Agency), Benjamin McCormick, Mary Popeck

In this report, the authors describe work to develop standards for automated remediation of vulnerabilities and compliance issues on DoD networked systems.

Topics: Cyber-Physical Systems

Authors: Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman

This presentation considers the problem of verifying functional correctness of periodic Real-Time Embedded Software (RTES), a popular variant of RTES that execute periodic tasks in an order determined by Rate Monotonic Scheduling (RMS).

Topics: Acquisition Support

Authors: Sagar Chaki, Rita C. Creel, Jeff Davenport, Mike Kinney (National Security Agency), Benjamin McCormick, Mary Popeck

In this report, the authors describe work to develop standards for vulnerability and compliance remediation on DoD networked systems.

Topics: Software Architecture

Authors: Sagar Chaki, Arie Gurfinkel

In this report, the authors present COVERT, an automated framework for finding buffer overflows in C programs using software verification tools and techniques.

Authors: Sagar Chaki, James Ivers, Peter Lee, Kurt C. Wallnau, Noam Zeilberger

Sagar Chaki and others describe in this presentation an implementation of the approach that targets the Pin component technology, and presents experimental results on a collection of benchmarks.

Topics: Software Assurance

Authors: Sagar Chaki, James Ivers, Peter Lee, Kurt C. Wallnau, Noam Zeilberger

In this report, the authors present an approach to certify binary code against expressive policies to achieve the benefits of PCC and CMC.

Authors: Christopher J. Alberts, Eileen C. Forrester, Suzanne Garcia-Miller, Aaron Greenhouse, Jörgen Hansson (University of Skovde), James D. Herbsleb, James Ivers, Peter Lee, Richard C. Linger (Oak Ridge National Laboratory), Thomas A. Longstaff, Pratyusa K. Manadhata, William Anderson, B. Craig Meyers, Mike Phillips, Carol A. Sledge, James Smith, Kurt C. Wallnau, Gwendolyn H. Walton, J. Wing, Noam Zeilberger, Len Bass, Matt Bass, Philip J. Boxer, Lisa Brownsword, Sagar Chaki, Peter H. Feiler, David Fisher

This report describes the IRAD projects that were conducted during fiscal year 2006 (October 2005 through September 2006).

Authors: Sagar Chaki

Copper is a software model checker for concurrent message-passing C programs.

Authors: Sagar Chaki, Ofer Strichman

Paper from the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.

Authors: Sagar Chaki, Nishant Sinha

This report shows how L^F can be used for compositional regular failure language containment and deadlock detection, using non-circular and circular assume-guarantee rules.

Topics: Software Assurance

Authors: Sagar Chaki, Scott Hissam

In this report, the authors present a technique for certifying the safety of buffer manipulations in C programs.

Authors: Sagar Chaki

This 2006 report presents a technique that uses proofs to certify software.

Authors: Sagar Chaki, Scott Hissam

In this paper, the authors present an automated overflow detection technique based on model checking and iterative refinement.

Topics: Software Architecture

Authors: Sagar Chaki, Edmund Clarke, Natasha Sharygina, Nishant Sinha

This 2005 report describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system.

Authors: Rosann W. Collins, Rick Kazman, Richard C. Linger (Oak Ridge National Laboratory), Mark Pleszkoch, Stacy J. Prowell, Natasha Sharygina, Kurt C. Wallnau, Gwendolyn H. Walton, Charles B. Weinstock, Lutz Wrage, Sagar Chaki, Peter H. Feiler, John B. Goodenough, Aaron Greenhouse, Jörgen Hansson (University of Skovde), Alan R. Hevner (University of South Florida), John J. Hudak, Angel Jordan

This report describes the IR&D projects that were conducted during fiscal year 2005 (October 2004 through September 2005). In addition, this report provides information on what the SEI has learned in its role as a technology scout for developments over the past year in the field of software engineering.

Authors: Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau

Presented: August 2005

Authors: Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau

Model checking is a promising technology for verifying critical behavior of software. However, software model checking is hamstrung by scalability issues and is difficult for software engineers to use directly. ComFoRT addresses both of these challenges.

Authors: Sagar Chaki, Edmund Clarke

Predicate abstraction is a popular abstraction technique employed in formal software verification. Experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.