A Security-Typed Language for Enforcing Non-Interference in Multi-Level Military Command and Control Systems

Military command and control systems handle data with different secrecy levels, even when the software runs in one shared networked setting. That mix can cause a security flaw. A program can be correct in how it works, but still let higher secrecy data affect lower secrecy results or messages. This work suggests ST-C2. It is a small programming language that uses security types. It uses three confidentiality tiers. Unclassified is L. Secret is M. Top Secret is H. ST-C2 puts several pieces together. It uses security labels. It uses a lattice style information flow rule. It checks security types before running code. It also labels the program counter, or PC. In addition, it uses communication channels that carry security labels.
To improve the earlier idea, the design is spelled out more clearly. It gives the core syntax. It defines state based operational rules. It states security typing judgments. It also states a termination insensitive non-interference rule for programs that pass the type checks. A proof-of-concept type checker was written in Python. The evaluation used 17 test cases. Some were meant to be secure. Others were meant to be insecure. The tests cover direct information moves. They also cover implicit moves that show up through PC labels. They include labeled communication channels as well.
In the end, the prototype handled all 17 cases the right way. On the chosen benchmark, the result was 100 percent. No false positives and no false negatives were seen. A basic timing check also matched an almost linear pattern for the small checking step as the number of checks rose. These results are only early. They do not replace a full compiler. They also do not act like a full operational military C2 system. Still, the study adds a formal language model aimed at C2 needs. It links well known programming language security tools to an explicit noninterference goal. It also sets a starting point for later work and implementation.

Security-Typed Programming Language, Theory of Programming Languages, Information Flow Security, Non-Interference, Static Type Checking, Military Command and Control, Compiler.

1. Bell, D. E., & LaPadula, L. J. (1973). Secure computer systems: Mathematical foundations. MITRE Corporation. [Google Scholar] [Crossref]

2. Denning, D. E. (1976). A lattice model of secure information flow. Communications of the ACM, 19(5), 236–243. https://doi.org/10.1145/360051.360056 [Google Scholar] [Crossref]

3. Goguen, J. A., & Meseguer, J. (1982). Security policies and security models. In 1982 IEEE Symposium on Security and Privacy (pp. 11–20). IEEE. [Google Scholar] [Crossref]

4. Myers, A. C. (1999). JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 228–241). ACM. https://doi.org/10.1145/292540.292561 [Google Scholar] [Crossref]

5. Pierce, B. C. (2002). Types and programming languages. MIT Press. [Google Scholar] [Crossref]

6. Russo, A., & Sabelfeld, A. (2010). Dynamic vs. static flow-sensitive security analysis. In 2010 IEEE 23rd Computer Security Foundations Symposium (pp. 186–199). IEEE. https://doi.org/10.1109/CSF.2010.21 [Google Scholar] [Crossref]

7. Sabelfeld, A., & Myers, A. C. (2003). Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), 5–19. https://doi.org/10.1109/JSAC.2002.806121 [Google Scholar] [Crossref]

8. Sabelfeld, A., & Sands, D. (2009). Declassification: Dimensions and principles. Journal of Computer Security, 17(5), 995–1023. https://doi.org/10.3233/JCS-2009-0353 [Google Scholar] [Crossref]

9. Smith, G. (2007). Formal models of information flow. In Foundations of Security Analysis and Design V (pp. 1–43). Springer. https://doi.org/10.1007/978-3-540-75227-9_1 [Google Scholar] [Crossref]

10. Volpano, D., Smith, G., & Irvine, C. (1996). A sound type system for secure flow analysis. Journal of Computer Security, 4(2–3), 167–187. https://doi.org/10.3233/JCS-1996-42-305 [Google Scholar] [Crossref]

• What the Desert Fathers Teach Data Scientists: Ancient Ascetic Principles for Ethical Machine-Learning Practice
• Comparative Analysis of Some Machine Learning Algorithms for the Classification of Ransomware
• Comparative Performance Analysis of Some Priority Queue Variants in Dijkstra’s Algorithm
• Transfer Learning in Detecting E-Assessment Malpractice from a Proctored Video Recordings.
• Dual-Modal Detection of Parkinson’s Disease: A Clinical Framework and Deep Learning Approach Using NeuroParkNet