2000 · 73 citations · 69 references
ComputingComputer ScienceComputer SystemsComputer SecurityFormal MethodsOperating SystemsDeductive VerificationOperating System SecurityStatic Vulnerability AnalysisTrusted BootTrusted ComputingTrusted Execution Environment SecurityTrusted Execution EnvironmentsTrusted Systems
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . i Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iv List of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .viii 1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 1.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Organization of Dissertation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 2.1 Safety Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . ....
69
An axiomatic basis for computer programming
C. A. R. Hoare · Communications of the ACM · 1969 · 3.9K citations · Full text
The MD5 Message-Digest Algorithm
Rivest · Medical Entomology and Zoology · 1992 · 2.9K citations
A theory of type polymorphism in programming
Robin Milner · Journal of Computer and System Sciences · 1978 · 2.2K citations · Full text
A lattice model of secure information flow
Dorothy E. Denning · Communications of the ACM · 1976 · 1.9K citations · Full text