Software Engineering Section

Code 5546 is the Software Engineering Section in the Center for High Assurance Computer Systems Branch of the Information Technology Division.

The section's mission is to conduct research in and to develop technology for high assurance software. The primary thrust of the research is the formulation of mathematically based methods, models, algorithms, and theories supporting both the construction as well as the analysis of software at different levels of abstraction from requirements through binary code. Researchers in the section work closely with developers and evaluators of Naval and other government systems to transfer the results of the section's research to software practice.

Model-Based Software Development and Analysis

  • Requirements Specification, Validation and Verification
  • Compositional Software Construction and Verification
  • Assertion-Based Analysis of Software Models
  • Hardware/Software Co-Design
  • Fault-Tolerant Computing
  • Real-Time Computing

Secure Software Construction and Analysis

  • Security Models
  • Code Verification
  • Security Policy Specification and Analysis
  • Security Vulnerability Detection and Remediation
  • Certification Artifacts
    • Secure Embedded Devices
    • Cross Domain Solutions

Specialized Theorem Proving

  • Theorem Proving Support in Special Domains
  • Mechanized Support for Human Style Proofs

Binary Analysis

  • Binary Reverse Engineering
  • Vulnerability Analysis and Remediation
  • Malicious Code Detection

Middleware for Secure and Dependable Distributed Systems

  • Multi-Agent Systems
  • Agent-Oriented Software engineering
  • Reconfigurable and Secure Middleware
  • Transformational Code Development
  • Formal Analysis of Software Engineering Artifacts

Products

  • Software Cost Reduction (SCR): Requirements Method and Toolset
  • Salsa (SCR Abstract Language Simple Analyzer): Automatic Property Checker for Software Artifacts
  • Timed Automata Modeling Environment (TAME): Tool for Proving Properties of Automata Models and of Programs
  • Language and Environment for Modeling Algorithms (LEMA): Toolset for Verifying Algorithms
  • Secure Infrastructure for Networked Systems (SINS): Infrastructure for Secure Middleware
  • PoliAna: Policy Analysis Toolset