Alley Stoughton
ABSTRACT
We report on a case study in secure programming, focusing on the design, implementation and auditing of programs for playing the board game Battleship. We begin by precisely defining the security of Battleship programs, borrowing ideas from theoretical cryptography. We then consider three implementations of Battleship: one in Concurrent ML featuring a trusted referee; one in Haskell/LIO using information flow control to avoid needing a trusted referee; and one in Concurrent ML using access control to avoid needing such a referee. All three implementations employ data abstraction in key ways.
- O. Arden, S. Chong, A. Myers, K. Vikram, and D. Zhang. Jif Distribution, Version 3.4.1, April 2013. www.cs.cornell.edu/jif.Google Scholar
- A. Askarov and A. Sabelfeld. Security-typed languages for implementation of cryptographic protocols: A case study. In Proc. of the 10th European Conference on Research in Computer Security, ESORICS'05, pages 197--221. Springer-Verlag, 2005. Google ScholarDigital Library
- R. Canetti. Security and composition of multi-party cryptographic protocols. J. Cryptology, 13(1):143--202, 2000.Google ScholarDigital Library
- D. B. Giffin, A. Levy, D. Stefan, D. Terei, D. Mazières, J. C. Mitchell, and A. Russo. Hails: Protecting data privacy in untrusted web applications. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation, OSDI'12, pages 47--60, Berkeley, CA, USA, 2012. USENIX Association. Google ScholarDigital Library
- C. Hriţcu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett. All your IFCException are belong to us. In Proc. of the 2013 IEEE Symposium on Security and Privacy, SP '13, pages 3--17. IEEE Computer Society, 2013. Google ScholarDigital Library
- B. W. Lampson. Protection. In Proc. of the Fifth Princeton Symposium on Information Sciences and Systems, pages 437--443. Princeton University, 1971. Reprinted in Operating Systems Review, 8, 1, January 1974, pages 18--24.Google Scholar
- J. Liu, M. D. George, K. Vikram, X. Qi, L. Waye, and A. C. Myers. Fabric: A platform for secure distributed computation and storage. In Proc. of the ACM Symposium on Operating Systems Principles, pages 321--334. ACM, 2009. Google ScholarDigital Library
- R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML---Revised 1997. MIT Press, 1997. Google ScholarDigital Library
- A. C. Myers. JFlow: Practical mostly-static information flow control. In Proc. of the 26th ACM Symposium on Principles of Programming Languages (POPL), pages 228--241. ACM, 1999. Google ScholarDigital Library
- A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proc. of the 16th ACM Symposium on Operating System Principles (SOSP), pages 129--142. ACM, 1997. Google ScholarDigital Library
- J. H. Reppy. Concurrent Programming in ML. Cambridge University Press, 1999. Google ScholarDigital Library
- A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, Sept. 2006. Google ScholarDigital Library
- D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières. Flexible dynamic information flow control in Haskell. SIGPLAN Notices, 46(12):95--106, Sept. 2011. Google ScholarDigital Library
- D. Stefan, A. Russo, D. Mazières, and J. C. Mitchell. Disjunction category labels. In Proc. of the 16th Nordic Conference on Information Security Technology for Applications, NordSec'11, pages 223--239. Springer-Verlag, 2012. Google ScholarDigital Library
- D. Terei, S. Marlow, S. Peyton Jones, and D. Mazières. Safe Haskell. In Proc. of the 2012 Haskell Symposium, pages 137--148. ACM, 2012. Google ScholarDigital Library
- S. Zdancewic. Challenges for information-flow security. In Proc. Programming Language Interference and Dependence (PLID), 2004.Google Scholar
- L. Zheng, S. Chong, A. C. Myers, and S. Zdancewic. Using replication and partitioning to build secure distributed systems. In Proc. of the 2003 IEEE Symposium on Security and Privacy, pages 236--250. IEEE, 2003. Google ScholarDigital Library
Index Terms
- You Sank My Battleship!: A Case Study in Secure Programming
Recommendations
Flow-Limited Authorization
CSF '15: Proceedings of the 2015 IEEE 28th Computer Security Foundations SymposiumBecause information flow control mechanisms often rely on an underlying authorization mechanism, their security guarantees can be subverted by weaknesses in authorization. Conversely, the security of authorization can be subverted by information flows ...
Taxonomy and analysis of security protocols for Internet of Things
AbstractThe Internet of Things (IoT) is a system of physical as well as virtual objects (each with networking capabilities incorporated) that are interconnected to exchange and collect information locally or remotely over the Internet. Since ...
Highlights- We first discuss essential security requirements that are needed to secure IoT environment. We also discuss the threat model and various attacks related to ...
Access Control and Information Flow Control for Web Services Security
With the advancement of web services technology, security has become an increasingly important issue. Various security standards have been developed to secure web services at the transport and message level, but application level has received less ...
Reviews
Michael G. Murphy
A secure programming case study focusing on the board game Battleship is the focus of this interesting and significant paper. Security is defined with techniques from theoretical cryptography. Three Battleship implementations are considered: one with a trusted referee; one with information flow control (IFC); and one with access control (AC). After discussing the motivation for the case study, the second section provides the rules for Battleship, the underlying client/server architecture, and how program security is defined. Next, the third, fourth, and fifth sections describe the various implementations, which are a trusted referee implementation in concurrent ML (CML), an IFC implementation in Haskell/LIO, and an AC implementation in CML, respectively. Section 6 presents conclusions based on the case study and indicates future research directions. An observation in section 6 regarding module sandboxing (requiring library access and communication only through interfaces) is a promising feature for ML/CML. Source code is available to download in .tqz format at http://www.ll.mit.edu/mission/cybersec/CST/CSTcorpora/Cybersystemscorpora.html. There are ten helpful figures that offer structural and flow items, Battleship board layouts with annotations, and code snippets. Seventeen key references lay out the foundations leading to the approach and alternatives chosen by the authors. This insightful and well-written report is a valuable contribution to the area of secure programming and is written to benefit a variety of readers while focusing on an understandable application over theory. It will be interesting to see subsequent work by these authors and other researchers who seek to push the envelope on this important topic. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments