Communications - February 2009

4. WebIL

After the Swift compiler has checked information flows in the Jif program, the program is translated to an intermediate language, WebIL. WebIL extends Java with placement annotations for both code and data. Placement annotations define constraints on where code and data may be replicated. These constraints may be due to security restrictions derived from the Jif code, or to architectural restrictions (for example, calls to a database must occur on the server, and calls to the UI must occur on the client).

Whereas Jif allows expression and enforcement of rich security policies from the DLM, ¹⁴ the WebIL language is concerned only with the placement of code and data onto two host machines, the server and the client. Thus, when translating to WebIL, the compiler projects annotations from the rich space of DLM security policies down to the much smaller space of placement constraints.

Using the placement constraint annotations, the compiler chooses a partitioning of the WebIL code. A partitioning is an assignment of every statement and field to a host machine or machines on which the statement will execute, or on which the field will be replicated.

WebIL can be used as a source language in its own right, allowing programmers to develop Web applications in a Java-like programming language with GUI support. This approach has benefits over traditional Web application programming, but does not enforce security as fully as Swift.

4. 1. Placement annotations

Each statement and field declaration in WebIL has one of nine possible placement annotations, shown in Table 1: C, S, Sh, C?Sh, C?S?, CS, CS?, C?S,and CSh. Each annotation defines the possible placements for the field or statement. There are three possible placements: client, server, and both. The intuition is that C and S mean the statement or field must be placed on the client and server, respectively, whereas C? and S? mean it is optional. An h signifies high integrity. Figure 3 shows the result of translating Guess-a-Number into WebIL, including placement constraints.

The placement of a field declaration indicates which host or hosts the field data is replicated onto. For example, if a field has the placement server, that field is stored only on the server; if it has the placement both, it is replicated on both client and server.

Similarly, the placement of a statement indicates what machines its computation is replicated onto. For compound statements such as conditionals and loops, the placement indicates the hosts for evaluating the test expression. On line 11 of Figure 3, the comparison of the guess to the secret number is given the annotation Sh, meaning that it must occur only on the server. Intuitively, this is the expected placement: the secret number cannot be sent to the client, so the comparison must occur on the server. On line 3, the annotation C?S? indicates that there is no constraint on where to test that num is non-null; that test may occur on the client, server, or both.

On statements, the annotations Sh, C?Sh, and CSh mark high-integrity code that must be executed on the server. The Swift compiler marks statements as high-integrity if

their execution may affect data that the client should not be able to influence. For example, lines 5–14 of Figure 3 are high-integrity. The client’s ability to initiate execution of high-integrity statements is restricted by Swift run-time mechanisms.

4. 2. translation from Jif to WebIL

When the compiler translates from Jif to WebIL code, it replaces DLM security policies with corresponding placement constraint annotations. Based on the security policies of the Jif code, the compiler chooses annotations that ensure code and data are placed on the client only if the client cannot violate the security of the program.

Therefore, translation ensures that data may be placed on a client only if the security policies indicate that the data may be read by the principal client; data may originate from the client only if the security policies indicate that the data is permitted to be written by the principal client. Similar restrictions apply to code: code may execute on the client only if the execution of the code reveals only information

table 1: WebIL placement constraint annotations.

annotation Possible placements C {client} S {server} Sh {server} CS {both} CSh {both} CS? {client, both} C?S {server, both} C?Sh {server, both} C?S? {client, server, both}