Information Technology Reference
In-Depth Information
investigating existing formal methods. From that experience and long-time re-
investigation, we propose Isabelle/Isar as a good candidate in further developing
of Chinese secure operating systems.
References
1. Leveson, N.G.: Geust Editor's Introduction: Formal Methods in Software Engi-
neering. IEEE Transactions in Software Engineering. September (1990) 929-931
2. Wenzel, M.: Isabelle/Isar - A Versatile Environment for Human-Readable Formal
Proof Documents. PhD thesis. Institute f
u
r Informatik, Technische Universit
a
t
M
u
nchen. (2002)
3. Bell, D.E., La Padula, L.J.: Secure Computer System: Unified Exposition and
Multics Interpretation. MITRE Report, MTR-2997 Rev.1. (1976)
4. CSC-STD-001-83, Department of Defense Standard. Department of Defense
Trusted Computer System Evaluation Criteria. National Computer Security Cen-
ter, Ft. Meade, MD. USA (1985)
5. Waldhart, N.A.: The Army Secure Operating System. 1990 IEEE Symposium on
Security and Privacy (1990) 50-60
6. Saydjari, O.S.: LOCK: An Historical Perspective, 18th Annual Computer Security
Applications Conference (2002) 96-108
7. Good, D., Akers, R., Smith, L.: Report on Gypsy 2.05. Tech. Rept. ICSCA-CMP-
48. Institute for Computer Science and Computing Applications. The University
of Texas at Austin (1986)
8. Wu, Y., Shi, W., Liang, H., Shang, Q., Yuan, C., Liang, B.: Security On-demand
Architecture with Multiple Modules Support. Information Security Practice and
Experience, First International Conference.Singapore (2005) 121-131
9. Mayer, F.L.: An Interpretation of a Refined Bell-La. Padula Model for the Tmach
Kernel. Fourth Aerospace Computer Security Applications Conference (1988)
10. Bell, D.E.: Secure Computer Systems: A Network Interpretation. Second Aerospace
Computer Security Conference (1986) 32-39
11. Liang, B., Liu, H., Shi, W., Wu, Y.: Enforcing the Principle of Least Privilege
with a State-Based Privilege Control Model. Information Security Practice and
Experience, First International Conference.Singapore (2005) 109-120
12. Spivey, J.M.: Understanding Z: A Spcification language and its formal semantics,
volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge Uni-
versity Press (1988)
13. Meisels, I., Saaltink, M.: The Z/EVES Reference Manual (for Version 1.5). Tech-
nical Report, TR-97-5492-03d. ORA Canada. (1997)
14. Havelund, K, Lowry, M., Penix, J.: Formal Analysis of A Space Craft Controller
Using SPIN. IEEE Transactions on Software Engineering. Vol. 27, no. 8 (2001)
749-765
15. Pecheur, C., Simmons, R.: From Livingstone to SMV: Formal Verification for Au-
tonomous Spacecrafts. In Proceedings of First Goddard Workshop on Formal Ap-
proaches to Agent-Based Systems. NASA Goddard (2000) 103-113
