This research project consists of identifying and modeling formal guarantees for NASA's DTN implementation. This document focuses on identifying security concerns and their ad hoc solutions, and researching how other network protocols have abstracted. Hopefully this can provide some insight on where we can start to model our DTN's behavior and what properties to target. The project should broadly be divided in the following steps:
- Model NASA's implementation of DTN (abstraction)
- Mechanize a general network calculus that targets DTN
- Prove some scheduling property that's provided guarantees through the network calculus in our NASA DTN abstraction.
- Find out if NASA's framework follows such properties, if so then good! If not then tell them that.
Delay-tolerant networks address technical issues in heterogeneous networks that lack continuous network connectivity, i.e. latency issues. Technically, DTNs are characterized by their lack of connectivity.
NASA's ION (Interplanetary Overlay Network) is the implementation of the DTN architecture we will be working with. Context for the full series of lectures on ION can be found here, and notes on the lectures are here. These are the main takeaways in regards to properties to guarantee:
The NASA Glenn paper has made our initial plan way more complicated than initially expected... please read through NASADTN to get details on how our plan changes.
These issues are outlined in the Wiki page, and do not necessarily imply the properties we seek to prove in the Coq model, but general concerns.
- Networks without bi-directional end-to-end paths between devices hinders complicated cryptographic protocols and key exchanges, meaning each device must identify other intermittently visible devides. This is an authentication problem.
- The solution is to use ad hoc certificates with PKI schemes.
- Identity-based encryption allows nodes to receive information encrypted with their public identifier.
- The use of tamper-evident tables with a gossiping protocol.
Ideally, we don't want to rely on ad hoc certificates. For some context on formal guarantees, we can look at how RTNs have been tackled.
This HAL paper on Formal Verification of Real-time Networks will be the main reference for this section. This paper provides a network calculus for checking bounds on delays. This calculus can be mechanized to provide delay certificates through Coq rather than relying on ad hoc methods. There's still a property we have to check for the actual implementation of the DTN, and that could be static-priority scheduling.
Some important (and not so important) notes are found over here. This includes analyzing and summarizing research papers that could be used as reference, and describing the current NASA proposal we're working with. The two main notes that matter are the network calculus analysis and the NASA Glenn proposal.