Battleship

We implement a simplified version of the classical Battleship game, which has already some history as an IFC example. The client uses the browser to play against the server and both players want hide the exact position of their ships on a grid. Both sides trust each other to correctly follow the rules of the game, so we are only concerned about confidentiality and not integrity. A desirable IFC policy for this game is to mark the values indicating individual ship positions as confidential and all parameters and return values of RPC functions as public, so that confidential information is not allowed to pass the barrier between the browser and the server. This allows us to re-use the same security policy on both sides. The game rules require declassification, since the response to a shot requires disclosure of one bit of information (“hit” or “miss”) to the other player per round. On each side we have to perform declassification twice: firstly for the hit/miss response to a shot, as it directly depends on the presence of a ship at that location, and secondly for indicating to the opponent if a player is defeated, which requires to test all occupied cells. The latter can also be done locally, but for implementation reasons players report their own defeat to the opponent. The following example shows this for the client-side:

let serverShotResult = {

shot = response.shot;

hit = DeclassifyBool !serverTarget.occupied;

defeated = DeclassifyBool clientDefeated }

The scenario consists of 250 F# and 6342 generated Javascript LOCs.