Verifying Code toward Trustworthy Software

키워드

참고문헌 (70)

1. G. C. Necula, "Proof-carrying code", Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.106~119 (1997)
2. G. C. Necula, "Safe, untrusted agents using proof-carrying code", Mobile Agents and Security, pp.61~91 (1998)
3. A. W. Appel, "Foundational proof-carrying code", Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, pp.247~256 (2001)
4. A. W. Appel, "An indexed model of recursive types for foundational proof-carrying code", ACM Transactions on Programming Languages and Systems, 23(5), pp.657~683 (2001)[DOI]
5. J. Vanegue, "The weird machines in proof-carrying code", Proceedings of the IEEE Security and Privacy Workshops, pp.209~213 (2014)
6. X. Leroy, "Formal verification of a realistic compiler", Communications of the ACM, 52(7), pp.107~115 (2009)[DOI]
7. G. Morrisett, "From system F to typed assembly language", ACM Transactions on Programming Languages and Systems, 21(3), pp.527~568 (1999)[DOI]
8. K. Crary, "Talx86: a realistic typed assembly language", Proceedings of ACM SIGPLAN Workshop on Compiler Support for System Software, pp.25~35 (1999)
9. G. Morrisett, "Typed assembly language", Advanced Topics in Types and Programming Languages, pp.141~176 (2005)
10. F. Perry, "Fault-tolerant typed assembly language", ACM SIGPLAN Notices, 42, pp.42~53 (2007)[DOI]
11. C. Lattner, "LLVM: a compilation framework for lifelong program analysis & transformation", Proceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization, pp.75~ (2004)
12. M. Patrignani, "Secure compilation to protected module architectures", ACM Transactions on Programming Languages and Systems, 37(2) (2015)
13. H. Xi, "A dependently typed assembly language", ACM SIGPLAN Notices, 36(10), pp.169~180 (2001)[DOI]
14. U. Norell, "Towards a practical programming language based on dependent type theory", pp.2007
15. L. Augustsson, "Cayenne: a language with dependent types", Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming, pp.239~250 (1998)
16. The Coq proof assistant reference manual: Version 6, "B. Barras", INRIA, ~, pp.Report No. RT-0203 (1997)
17. A. Chlipala, "Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant" (2013), MIT Press
18. C. McBride, "Epigram: practical programming with dependent types", Advanced Functional Programming, pp.130~170 (2004)
19. E. Brady, "Idris, a general-purpose dependently typed programming language: design and implementation", Journal of Functional Programming, 23(5), pp.552~593 (2013)[DOI]
20. A. Jeffrey, "Dependently typed web client applications", Practical Aspects of Declarative Languages, pp.228~243 (2013)
21. G. Huet, "30 years of research and development around Coq", ACM SIGPLAN Notices, 49(1), pp.249~249 (2014)[DOI]
22. A. Athalye, "CoqIOA: a formalization of I", O automata in the Coq proof assistant, Massachusetts Institute of Technology, 2017
23. S. Chatzikyriakidis, "Natural language reasoning using proof assistant technology: rich typing and beyond", Proceedings of the EACL 2014 Workshop on Type Theory and Natural Language Semantics, pp.37~45 (2014)
24. J. C. Reynolds, "Separation logic: a logic for shared mutable data structures", Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, pp.55~74 (2002)
25. D. Distefano, "A local shape analysis based on separation logic", Tools and Algorithms for the Construction and Analysis of Systems, pp.287~302 (2006)
26. J. Berdine, "Symbolic execution with separation logic", Proceedings of Asian Symposium on Programming Languages and Systems, pp.52~68 (2005)
27. J. Berdine, "Smallfoot: modular automatic assertion checking with separation logic", Formal Methods for Components and Objects, pp.115~137 (2005)
28. X. Qiu, "Natural proofs for structure, data, and separation", ACM SIGPLAN Notices, 48(6), pp.231~242 (2013)[DOI]
29. E. Pek, "Natural proofs for data structure manipulation in C using separation logic", ACM SIGPLAN Notices, 49(6), pp.440~451 (2014)[DOI]
30. E. Cohen, "VCC: a practical system for verifying concurrent C", Theorem Proving in Higher Order Logics, pp.23~42 (2009)
31. A. Silberschatz, "Operating System Concepts Essentials" (2014), John Wiley & Sons
32. R. Wahbe, "Efficient software based fault isolation", ACM SIGOPS Operating Systems Review, 27(5), pp.203~216 (1994)
33. J. A. Kroll, "Portable software fault isolation", Proceedings of the IEEE 27th Computer Security Foundations Symposium, pp.18~32 (2014)
34. A. Sabelfeld, "Language-based information-flow security", IEEE Journal on Selected Areas in Communications, 21(1), pp.5~19 (2003)[DOI]
35. D. Costanzo, "End-to-end verification of information-flow security for C and assembly programs", ACM SIGPLAN Notices, 51(6), pp.648~664 (2016)[DOI]
36. G. Doychev, "Cacheaudit: a tool for the static analysis of cache side channels", ACM Transactions on Information and System Security, 18(1) (2015)
37. M. Sutton, "Fuzzing: Brute Force Vulnerability Discovery" (2007), Pearson Education
38. A. Takanen, "Fuzzing for Software Security Testing and Quality Assurance" (2008), Artech House
39. J. W. Duran, "A report on random testing", Proceedings of the 5th International Conference on Software Engineering, pp.179~183 (1981)
40. P. Godefroid, "Grammar-based whitebox fuzzing", ACM SIGPLAN Notices, 43(6), pp.206~215 (2008)[DOI]
41. N. Stephens, "Driller: augmenting fuzzing through selective symbolic execution", Proceedings of the 23rd Annual Network and Distributed System Security Symposium, pp.1~16 (2016)
42. I. Goldberg, "A secure environment for untrusted helper applications: confining the wily hacker", Proceedings of the 6th Conference on USENIX Security Symposium Focusing on Applications of Cryptography (1996)
43. S. Van Acker, "JavaScript sandboxing: isolating and restricting client-side JavaScript", Foundations of Security Analysis and Design VIII, pp.32~86 (2015)
44. J. G. Politz, "ADsafety: type-based verification of JavaScript sandboxing", Proceedings of the 20th USENIX Security Symposium (2011)
45. P. Agten, "JSand: complete clientside sandboxing of third-party JavaScript without browser modifications", Proceedings of the 28th Annual Computer Security Applications Conference, pp.1~10 (2012)
46. P. H. Phung, "A two-tier sandbox architecture for untrusted JavaScript", Proceedings of the Workshop on JavaScript Tools, pp.1~10 (2012)
47. W. Enck, "TaintDroid: an information-flow tracking system for real time privacy monitoring on smartphones", ACM Transactions on Computer Systems, 32(2) (2014)
48. D. Hedin, "JSFlow: tracking information ow in JavaScript and its APIs", Proceedings of the 29th Annual ACM Symposium on Applied Computing, pp.1663~1671 (2014)
49. K. Claessen, "QuickCheck: a lightweight tool for random testing of Haskell programs", ACM SIGPLAN notices, 46(4), pp.53~64 (2011)
50. C. Pacheco, "Randoop: feedback-directed random testing for Java", Companion to the 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, pp.815~816 (2007)
51. P. Godefroid, "DART: directed automated random testing", ACM SIGPLAN Notices, 40(6), pp.213~223 (2005)
52. X. Leroy, "Formal certification of a compiler back-end or: programming a compiler with a proof assistant", ACM SIGPLAN Notices, 41(1), pp.42~54 (2006)
53. J. Zhao, "Formalizing the LLVM intermediate representation for verified program transformations", ACM SIGPLAN Notices, 47(1), pp.427~440 (2012)[DOI]
54. L. Gu, "CertiKOS: a certified kernel for secure cloud computing", Proceedings of the 2nd Asia-Pacific Workshop on Systems (2011)
55. R. Gu, "Deep specifications and certified abstraction layers", ACM SIGPLAN Notices, 50(1), pp.595~608 (2015)[DOI]
56. G. Klein, "seL4: formal verification of an OS kernel", Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp.207~220 (2009)
57. G. Klein, "Provably trustworthy systems", Philosophical Transactions of the Royal Society A, 375(2104) (2017)
58. R. E. Korf, "Depth-first iterative-deepening: an optimal admissible tree search", Artificial Intelligence, 27(1), pp.97~109 (1985)[DOI]
59. S. J. Garland, "An overview of LP, the Larch Prover", Rewriting Techniques and Applications, pp.137~151 (1989)
60. A. Anand, "CertiCoq: a verified compiler for Coq", Proceedings of the 3rd International Workshop on Coq for Programming Languages (2017)
61. HOL: A Proof Assistant for Higher-Order Logic, "Isabelle", pp.2002, T. Nipkow
62. M. Wenzel, "Isabelle as document-oriented proof assistant", Intelligent Computer Mathematics, pp.244~259 (2011)
63. P. B. Jackson, "The Nuprl Proof Development System (Version 4.2) Reference Manual and User's Guide", Cornell University, ~ (1994)
64. S. Owre, "PVS: combining specification, proof checking, and model checking", Computer Aided Verification, pp.411~414 (1996)
65. F. Pfenning, "System description: Twelf: a meta-logical framework for deductive systems", Automated Deduction (CADE-16), pp.202~206 (1999)
66. C. Schurmann, "The Twelf proof assistant", Theorem Proving in Higher Order Logics, pp.79~83 (2009)
67. "REMS: rigorous engineering of mainstream systems"[URL]
68. J. Madey, "Book Review: the Z notation: a reference manual: JM Spivey. Prentice Hall International, Hemel Hempstead, United Kingdom, 1989", Science of Computer Programming, 15(2, pp.3) (1990), 253~255
69. D. Jackson, "Software Abstractions: Logic, Language, and Analysis" (2012), MIT Press
70. P. H. Feiler, "Model-based Engineering with AADL: an Introduction to the SAE Architecture Analysis & Design Language" (2012), Addison-Wesley

관련 논문AI추천