Reliable and effective ground-space communication is important for all NASA Missions. Security against malicious attacks has become a major issue. Our tool-supported development framework will enable the cost-effective, flexible development of correct and safe protocols for the specific needs of sustained Exploration Missions.
Benefit
CEV and other space vehicles require a reliable, safe and secure means of communication. Malicious attacks can jeopardize lives and mission success. Our approach enables the designer to cost-effectively develop verified and correct code for NASA's specific communication requirements (e.g., 20 min latency in communications to Mars).
Research Overview
Reliable and secure space communication software can only be developed with a unified end-to-end approach for the design, analysis, implementation, and certification, which is based upon rigorous logical and mathematical foundations. We are proposing a set of tools integrated into a software process which, given an intuitive, yet concise definition of all protocol requirements (e.g., using the Unified Modeling Language UML) can automatically perform the necessary analyses, support simulation, and automatically generate all required artifacts (code, documentation, certificates).
Because all software development steps are derived from one high level specification of the protocol and its properties, results of all analyses and the generated code are always in sync, thus eliminating many errors which would yield the communication software insecure. Formal-based tools for protocol optimization (e.g., to accommodate low bandwidths / low computational requirements), and automatic, tamper-proof certification can provide explicit guarantees about important reliability and security properties and the absence of implementation errors. A tremendous increase in correctness and reliability of the communication software can be obtained--technology which in turn leads to better security.
BackgroundAlthough secure communication protocols are in wide use (e.g., on the Internet), history has shown that many errors and vulnerabilities exist and have been exploited. Such security flaws may be introduced (or fail to be detected) during all stages of the software development cycle, like vulnerable encryption algorithms (design) or buffer overrun errors during implementation. Mission specific requirements (low bandwidth, high latency --20 minutes to Mars, and low on-board computational capabilities) pose additional severe challenges for secure communication software.
Right: Automatic, tamper-proof certification can provide explicit security guarantees