摘要: We explore the tension between adding functionality to create resilient software and minimizing make it more feasible formally verify software. To illustrate effects of this trade-off, we examine a tiny example in detail. show how code written with good style may be hard verify, specifically that test condition is troublesome. also "improved" an attempt verification straight-forward worsens failure characteristics. demonstrate effect actual situation, secure web server, thttpd, its design principles security features. discuss features introduce redundancies making harder, but present some formal feasible. conclude should designed necessary temptation oversimplify order resisted.
acm.org
computer.org
sci-hub.se 参考文章(8)
Michael J.C. Gordon, Programming language theory and its implementation Prentice Hall International (UK) Ltd.. ,(1988)
Phillip J. Windley, Michael D. Jones, Paul E. Black, Kelly M. Hall, Trent N. Larson, A Brief Introduction to Formal Methods ,(1996)
Paul E. Black, Phillip J. Windley, Inference rules for programming languages with side effects in expressions Lecture Notes in Computer Science. pp. 51- 60 ,(1996) , 10.1007/BFB0105396
P.E. Black, K.M. Hall, M.D. Jones, T.N. Larson, P.J. Windley, A brief introduction to formal methods [hardware design] custom integrated circuits conference. pp. 377- 380 ,(1996) , 10.1109/CICC.1996.510579
Frederick B. Cohen, A secure world-wide-web daemon Computers & Security. ,vol. 15, pp. 707- 724 ,(1996) , 10.1016/S0167-4048(96)00009-0
Z. Manna, R. Waldinger, The Logic of Computer Programming IEEE Transactions on Software Engineering. ,vol. SE-4, pp. 199- 229 ,(1978) , 10.1109/TSE.1978.231499
Edsger Wybe Dijkstra, A Discipline of Programming ,(1976)
Tony Hoare, An Axiomatic Basis for Computer Programming Communications of The ACM. ,vol. 12, ,(1969)