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.