Communications' Inside Risks columns have long stressed the importance of total-system awareness of riskful situations, some of which may be very difficult to identify in advance. Specifically, the desired properties of the total system should be specified as requirements. Those desired properties are called emergent properties, because they often cannot be derived solely from lower-layer component properties, and appear only with respect to the total system. Unfortunately, additional behavior of the total system may arise—which either defeats the ability to satisfy the desired properties, or demonstrates that the set of required properties was improperly specified.
In this column, I consider some cases in which total-system analysis is of vital importance, but generally very difficult to achieve with adequate assurance. Relevant failures may result from one event or even a combination of problems in hardware, software, networks, operational environments, and of course actions by administrators, users, and misusers. All of the interactions among these entities need to be considered, evaluated, and if potentially deleterious, controlled by whatever means available. The problem to be confronted here is trying to analyze an entire system as a composition of its components, rather than just considering its components individually. In many cases, system failures tend to arise within the interactions and interdependencies among these components, depending on whether a system was designed modularly to minimize disruptive dependencies, with each module carefully specified.
Addressing this problem is a daunting endeavor, even for seasoned developers of critical systems. Whether explicitly defined or implicit, total-system requirements may be highly interdisciplinary, including stringent life-critical requirements for human safety; system survivability with reliability, robustness, resilience, recovery, and fault tolerance; many aspects of security and integrity; guaranteed real-time performance; forensics-worthy accountability, high-integrity evidence, and sound real-time and retrospective analysis; defenses against a wide ranges of physical, electronic, and other adversities; and coverage of numerous potential risks. Ideally, requirements should be very carefully specified at various architectural layers, preferably formally as much as possible in newly developed systems, and especially in particularly vulnerable components. Although this is usually not applicable to legacy systems, it is stated here as a farsighted goal for future developments.
Total-system architectures that must satisfy high-assurance requirements for trustworthiness may necessarily encompass much of what is described here. However, when executed on untrustworthy hardware and untrustworthy networks, the behavior of operating systems and application software should be considered with suspicion, as it suggests desirable emergent properties of the total system may have been compromised, or could easily be (resulting in adverse behavior).
Addressing this problem is a daunting endeavor, even for seasoned developers of critical systems.
An almost self-evident conclusion is that total-system trustworthiness with respect to realistic requirements under realistic assumptions is a very long-term goal that can never be completely achieved with any realistic sense of assurance. However, many efforts in that direction would be extremely valuable in attempting to withstand many adversities that are uncovered today. Several efforts currently under way are noted in this column, and seem to be small steps in that direction for new systems, although as previously mentioned, much less applicable to existing legacy systems. However, the enormity of the entire challenge should not discourage us from making structural improvements that could help overcome today's shortsightedness.
Hierarchically layered designs have considerable potential, but today are found mostly in well-designed operating systems and layered networking protocols. The concept has often been rejected because of erroneous nested efficiency arguments that can be overcome through good design practice. Formal specification languages and formal analysis of software and hardware have become much more widely applied in recent years. Formal specifications can also exist for system requirements, highlevel system architectures, hardware ISAs, and actual hardware. Here are just a few early examples (many others are omitted for brevity).
A long-term goal for the future would be to have hierarchical proofs (from the hardware up through hyper-visors, operating systems, and application code) to prove that specified total-system requirements (with stated assumptions) could be satisfied with some desired measure of assurance. There are still many potential pitfalls (incomplete requirements and specifications, inadequate development and assurance tools, sloppy programming, unreliable systems, malicious attacks, and so forth). However, assurance is necessary for each step along the way to this goal, as well as better analyses of entire systems. Unfortunately, that approach is not applicable to most legacy hardware-software systems, which suggests the long-term approach must be injected early into future technology developments.
The enormity of the entire challenge should not discourage us from making structural improvements that could help overcome today's shortsightedness.
Perhaps as an indication that more R&D is needed, DARPA is currently planning a new program called PROVERS: Pipelined Reasoning of Verifiers Enabling Robust Systems for extending formal methods to work at the scale of real systems.
Several relevant application areas in which the compromise of total-system attributes may be of great concern are considered here. In each case, there are difficulties in analyzing the relevant components, but also their embeddings into total systems; proving anything convincingly could be very difficult—if not generally impossible. Furthermore, even if a particular component could somehow be shown to be logically sound by itself (which often seems not to be the case), its compliant total-system behavior may be compromised by exploitation of hardware and operating system flaws that can undermine its integrity, or by poor application programs.
These examples expose just tips of multiple icebergs, but are intended to be suggestive of the difficulties that must be overcome.
There is also a desirability of having some independent sanity checks ensure the total-system results are correct.
In each of these cases, there is also a desirability of having some independent sanity checks ensure the total-system results are correct—or at least within realistic bounds—with respect to the stated requirements. An analogy in formal theorem proving is to use trustworthy proof checkers to check the proofs, although that still assumes the underlying assumptions and the proof checkers are correct and unbiased.
The desiderata were established many years ago, but are still not used widely in practice. A grossly oversimplified set might include something like this:
Significant progress is being made with some of the steps toward the desired long-term goal of total-system trustworthiness. Of course, all of this is still nowhere near enough, considering all the extrinsic problems we face. However, the goal is nevertheless worth pursuing for new critical systems—to the extent it is realistic. This suggests we must begin now to recognize the relevance of the overall long-term goal.
1. Berson, T.A. and Barksdale, G.L., Jr. KSOS: Development Methodology for a Secure Operating System, National Computer Conference, AFIPS Conference Proceedings 48 (1979), 365–371.
2. Clark, D. and Wilson, D.R. A comparison of commercial and military computer security policies. In Proceedings of the 1987 Symposium on Security and Privacy. IEEE Computer Society, Oakland, CA (Apr. 1987), 184–194.
3. Dave, N. A Unified Model for Hardware/Software Co-design, MIT Ph.D. thesis. 2011.
4. Dijkstra, E.W. The structure of the THE multiprogramming system. Commun. ACM 11, 5 (May 1968), 341–346.
5. Gligor, V.D. and Gavrila, S.I. Application-oriented security policies and their composition. In Proceedings of the 1998 Workshop on Security Paradigms, Cambridge, England, 1998.
6. Gu, R. et al. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI'16). (Nov. 2016), 653–669.
7. Heiser, G., Klein, G., and Andronick, J. seL4 in Australia: From research to real-world trustworthy systems. Commun. ACM 63, 4 (Apr. 2020), 72–75.
8. Klein, G. et al. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems 32, 1 (Feb. 2014).
9. Neumann, P.G. et al. A Provably Secure Operating System: The System, Its Applications, and Proofs. SRI International. 1980.
10. Neumann, P.G. Fundamental trustworthiness principles in CHERI. In A. Shrobe, D. Shrier, and A. Pentland, Eds. New Solutions for Cybersecurity. MIT Press/Connection Science (Jan. 2018); https://bit.ly/3kgxyt6
11. Nienhuis, K. et al. Rigorous engineering for hardware security: Formal modeling and proof in the CHERI design and implementation process. In Proceedings of the 36th IEEE Symposium on Security and Privacy, May 2020.
12. Parnas, D.L., Clements, P.C., and Weiss, D.M. The modular structure of complex systems. IEEE Transactions on Software Engineering SE-11, 3 (Mar 1985), 259–266.
13. Parnas, D.L. The real risks of artificial intelligence. Commun. ACM (Oct. 2017).
14. Robinson, L. and Levitt, K.N. Proof techniques for hierarchically structured programs. Commun. ACM 20, 4 (Apr. 1977), 271–283.
15. Watson, R.N.M. et al. Cambridge-SRI CHERI-ARM Morello and CHERI-RISC-V; https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
16. Yang et al. A2: Analog malicious hardware. In Proceedings of the 2016 IEEE Symposium on Security and Privacy. IEEE Computer Society.
a. This article refers to many additional references that deserve to be included here, such as Parnas's remarkably prescient early papers.
The Digital Library is published by the Association for Computing Machinery. Copyright © 2022 ACM, Inc.
No entries found