This section describes the differences in the Battleships implementation com-pared to the prevalent modus operandi as outlined in Section 1.2.
The first change was of course the conversion to a computer game. Since the game is designed around two players an obvious choice was to have to two players communicate over a network such as the Internet. Most computer games today based exclusively on networking use a client server architecture where the server has access to the world of the game, and the server is the only one who makes changes to the world based on the actions of the players.
This is the implementation used for this example.
To simplify the problem, a number of further changes were made. The players still place their ships on the board, but the players themselves are modeled as automatic processes, A and B, and randomly put ships with a size of one onto the board. The server “tosses a coin” using the random function of the gWhile language to decide who starts. The players also randomly decide on a set of coordinates to target and send off to the server.
After checking the coordinates the server sends a message to each player saying if it was a hit, if the game is over, and the coordinates.
The data sent to the players are in the implementation of the game simply ignored. In further implementation an extension to the gWhile language could allow this data to be written to the screen. In JIF as described in [ML00] this is handled through channels which handle any input and output from a program.
Key Declarations
Battleships has a large number of key declarations since both symmetric keys for communicating data and asymmetric keys for communicating the
symmetric keys are needed. Using parameterization of the key declarations, as discussed in Section 6.2, would halve the number of key declarations needed since each key declaration could be used for transmitting similar data to each of the two players. Furthermore, gWhile is a strongly typed language and necessitates a specific key declaration for each format of data that needs communicating.
# key declarations for the symmetric keys of A declareApppas{principal{},principal{},
principal{}}{A:all};
declareApptas{principal{},principal{},table{A:}}{A:
all};
declareAppbas{principal{},principal{},bool{}}{A:
all};
declareAppiias{principal{},principal{},int{}, int{}}{A:all};
declareAppbbiias{principal{},principal{},bool{}, bool{},int{}, int{}}{A:all};
Figure 5.17: Key declarations for the symmetric keys used in communi-cation betweenA and the server
Figure 5.17 shows the key declaration for the symmetric keys used in communication between the principal Aand the server. The keys based on these declarations have been referred to as session keys. Five further key declarations are declared for communication fromAto the server. They are used for the asymmetric keys necessary to communicate the session keys.
Key declarations for the corresponding communication between B and the server have also been declared.
The Players
The two player processes are carbon copies of each other with different prin-cipals. The discussion of one is therefore the same as the discussion of the other. In this description, only the process forA will be regarded.
The process starts with the definition of the five asymmetric keys. This is followed by the initialization, Figure 5.18. All the variables for the process have very restrictive labels, which is the most conservative configuration for data, and is used to prevent any illegal data flow. Among the initializations are of course the five symmetric keys, at the bottom of Figure 5.18, corre-sponding to the key declarations of Figure 5.17. In the description below, I do not simply note each time a key is instantiated and sent to the server, as this is done before every symmetric communication. There are a few cases which are a little different, these will be described briefly. Each session key is reused throughout the game after it is initially communicated.
server{A:}:=’S’, opponent{A:}:=’’, boardSizeH{A:}:= 10, boardSizeW{A:} := 10, board[10][10]{A:}, numShips{A:}:= 10, i{A:} := 0,
x{A:} := 0, y{A:} := 0,
myTurn{A:} :=false, done{A:}:=false, result{A:}:=false,
keykAppp{A: S}using Appp, keykAppt{A: S} usingAppt, keykAppb{A: S}using Appb, keykAppii{A: S}using Appii, keykAppbbii{A: S}usingAppbbii,
Figure 5.18: Initializations for process A
The process for a player starts by instantiating a key, the key kAppp.
This key is sent to the server which stores the principal for the player and the key. The server then uses the key to tell the player who his opponent is, the principal he is playing against. The first asymmetric communication serves both to send the first session key, but also to say that the principal is ready to play a game and who he is.
After receiving his opponent from the server, the player places his ships on the playing field, using the random function to find the coordinates where each ship is placed, and an if statement to check that two ships are not placed at the same location. The board is sent to the server which sends back a boolean true value once both boards have been received.
At this point the game itself starts and the session keys used within the game loop are communicated before the loop is entered. The loop uses the value of the variabledonewhich is initialized tofalseto iterate over, a new value of done is received after each player has had a turn to see if the game has concluded.
ifmyTurnthen
x :=random(boardSizeW);
y :=random(boardSizeH);
ssend(server,this,declassify(x,{}),declassify(y, {})){kAppii}
else ...
Figure 5.19: Targeting a pair of coordinates
Each turn the player receives a boolean value from the server, indicating whether it is his turn or not. If the player has his turn he generates a set of coordinates, Figure 5.19, and sends them to the server. In the player processes the coordinates have quite restrictive labels, and they have to be declassified for the server to be able to read them and send them to the opponent. If it is not his turn he waits to receive the coordinates from the server that his opponent is targetting. After receiving the coordinates, the player sends a boolean true value back to indicate that the server may declassify the board value at those coordinates, as described in Section 2.2.
Finally, regardless of turn, the player receives a message back from the server with the result of the shot, the new value of done, and the coordinates that were targeted.
As discussed in further detail in Section 6.2 there are several places in each player process, where user interaction could be injected.
The Server
The server has defined asymmetric keys for communicating with both play-ers. However, while the players have the public keys for communicating with the server, the server only have the private keys defined. The initializations for the server are shown in Figure 5.20. Notice in particular thatboard1 is the board for player 1, whilehit1 is the table showing where player 2 has shot, and hitShips1 contains the number of ships player 2 has hit. The very restrictive labels for the boards are used so thatS cannot access these variables outside the act for blocks.
The server process starts by receiving a session key from each principal.
The session key is used for sending each player as an opponent to the other.
Then the server receives the board from each player, and sends back the boolean valuetrueto indicate that the game is about to start.
Using the random function, Figure 5.21, the server selects which player starts, and enters the game loop. Just inside the loop a boolean value for each player indicating if the current turn is his, is sent as shown in Figure 5.22.
The game logic has been unfolded into two parts, each specific to one player. The two parts of the unfolding are equal except for the principals.
The description will be of the part which is for player 1, but it is equally applicable for player 2.
First the coordinates are received from player 1 and the server will act for that player for the rest of the turn. The coordinates are forwarded to player 2, who sends back the boolean valuetrue, to indicate that the server may act for him, Figure 5.23, and declassify the value for the board at the target coordinates. The declassified value is assigned to the variableboardValue.
boardValueis checked to see if there is a ship there, if a ship is present the table of shots from player 1 is checked. The shot is only a hit if there is a ship at the coordinates and player 1 has not shot there before. Remember that the coordinates are generated randomly so there is a chance that the same coordinates are generated several times in a game. In the board game version of Battleships you normally loose your turn if you shoot at coordinates you have shot at before, this is also the case in this implementation.
If there is a ship at the coordinates and it is the first time player 1 has targeted those coordinates then it is noted as a hit, the table of shots by player 1 is updated, and the number of ships hit by player 1 is incremented.
The value for done is set to true if the number of ships that have been hit by player 1 is equal to the total number of ships.
The server sends a message to each player with the result of the shot, the value of done, and the coordinates.
Finally, theturnvariable is updated to reflect that it is the other player’s turn.
player1{}:=’’, player2{}:=’’,
keykAppp{A: S} usingAppp, keykAppt{A: S}usingAppt, keykAppb{A: S} usingAppb, keykAppii{A: S} usingAppii, keykAppbbii{A: S}usingAppbbii, keykBppp{B: S}using Bppp, keykBppt{B: S}usingBppt, keykBppb{B: S}using Bppb, keykBppii{B: S}using Bppii, keykBppbbii{B: S}usingBppbbii, numShips{}:= 10,
# board for A and where B has shot board1[10][10]{A:},
hit1[10][10]{B: A}, hitShips1{B: A}:= 0,
# board for B and where A has shot board2[10][10]{B:},
hit2[10][10]{A: B}, hitShips2{A: B}:= 0, done{}:=false, hit{}:=false, boardValue{}:= 0, turn{}:= 0, x{}:= 0, y{}:= 0
Figure 5.20: Initializations for the server
# select the starting player turn :=random(2);
Figure 5.21: Using random to select the starting player
ssend(player1,this, turn = 1){kAppb};
Figure 5.22: Indicating turn of player with a boolean value
sreceive(this, player2,true;){kBppb} andactforBin boardValue :=declassify(board2[x][y],{})
endactfor;
Figure 5.23: Acting for player 2 to declassify board value at the target coordinates
5.6.1 Verification of Battleships
After the battleships program had been implemented it was checked using the implementation of the type checker. There were quite a few problems with respect to the annotation type system, not so much in the server, but in the player processes.
First and foremost there were a number of restrictions due to implicit flow. Since all the variable are defined with the very restrictive{A:} label, for principalA, all assignments inside branches or loops were restricted with this label in the block label. One such example is a simple communication statement as shown in Figure 5.24.
ssend(server,this,true){kAppb}
Figure 5.24: Simple communication statement which is affected by implicit information flow control
Since the block label within the game loop is {A :} the conditions for this statement, which from the type rule for the symmetric send statement is defined as
BtLivLki
which for each of the three fields becomes
BtL1 v Lk1
⇒ {A:} t {A:} v {}
⇒ {A:} v {}
BtL2 v Lk2
⇒ {A:} t {} v {}
⇒ {A:} v {}
BtL3 v Lk3
⇒ {A:} t {} v {}
⇒ {A:} v {}
A solution to this problem is to declassify the value of done in the con-dition for the game loop. The branch on the current turn has the same problem, due to the label of the myTurn variable. Since the statement in Figure 5.24 is inside both the game loop and the branch both cases must be declassified.
Declassifying both the condition of the game loop and of the turn branch solved the problems for the two last fields of the statement. However, the first field sends the value of serverto address the server. The variable has the restrictive label {A :}, but the field in the key declaration asks for the empty label. There are three possible solutions to this problem
1. Correct the key declaration to use the restrictive,{A:}, label 2. Declassify the value of server each time it is used
3. Set the label of server to the empty label
Option one is not viable, the implicit flow problems associated with the more restrictive label would be destructive to other fields in the key formats, for example in the declassification of the board value shown in Figure 5.23 of the server. The second option would work fine, and so would option three.
However, the dangers of letting the name of the server flow is not very great, and this option was chosen.
ifhitShips2 = numShipsthen done :=true
endif
Figure 5.25: An example of illegal implicit flow in the server In the server there was only one real problem found by the verification.
When the server checks if a player has hit all the ships of his opponent as shown in Figure 5.25.
As shown in Figure 5.20hitShips2has the label{A:B}. From the im-plicit flow conditiondonecannot be assigned a value inside the branch since it has the empty label. The solution is to declassify the value of hitShips2 to the empty label and accept the minute information leak associated with this; after all, both players have to know that the game is over.
5.6.2 Introducing Leaks
One of the purposes of the security annotations, as in the Decentralized La-bel Model, is to catch and disallow information leaks. To see some examples of this in action, some leaks are introduced into the example program.
Since there is no communication directly between the two players, only leaks from the server are regarded. The server is trusted to not behave maliciously, this means that the only point of interest is unintentional infor-mation leaks from the server.
One error that can be introduced which will result in a leak is on line 138 of Appendix C.2. The if condition
if declassify(hit2[x][y], {}) then
inside the block where the server acts for player 1, can be changed to if declassify(hit1[x][y], {}) then
The only change is that hit2 has been changed to hit1. This change would result in player 1 being able to shoot the same ship of player 2 several times, since the place where his shots is recorded is not the same that is checked. This is an example of a place where a bug can be used to cheat.
This bug will be caught. Since the owner of hit1is simply the principalB, or player 2, and the server is acting forA, player 1, the owner B cannot be removed from the label.
On the other hand, the obvious bug which would result in an information leak, on line 135 of Appendix C.2, cannot be caught. The bug is reproduced by changingboard2 toboard1 in
boardValue = declassify(board2[x][y], {})
At this point in the program the server is acting for both player 1 and player 2. To be able to catch this leak, the block where he acts for player 1 must be ended before he can start acting for player 2. This could, for exam-ple, be achieved with thedonotactfor statement suggested in Section 6.2.
With the constructs present in the language, the act for block of player 1 could end before the server begins acting for player 2. After declassifying the board value, the server would stop acting for player 2, and could get a new communication from player 1 to start acting for him again. This
would result in at least one extra communication per turn, but would catch this bug. The possible leaks shown in this section have been put into the file server-based-battleships-error.w which is available with the rest of the program as described in Appendix C.1.