2. 5. Client-side code

The compiler generates Java code to run on the client. This code is compiled to JavaScript code using the Google Web Toolkit (GW T). ⁸ The client- and server-side code uses various libraries: Swift’s run-time libraries, GWT, and the Java servlet framework.

A running Swift program uses an Ajax approach to securely implement the functionality defined by the original source code. From the browser’s perspective, the application is a single Web page, with most user actions, such as clicking on buttons, handled by JavaScript code. This code issues its own HTTP or HTTPS requests to the Web server, which executes Java code to compute XML responses.

if ( 1) for every confidentiality policy on y, there is one at least as restrictive on x (which is the case because alice → bob is at least as restrictive as alice → bob, alice) and ( 2) for every integrity policy on x, there is one at least as restrictive on y (which is the case because x has no integrity policy).

Suppose that x instead had the label {alice → client}. The information flow fromy to x would still be secure if the principal client acts for the principal bob, meaning that anything client does or says can be treated as coming from bob. In that case, alice → client is at least as restrictive as alice → bob. Acts-for relationships increase the expressive power of labels and allow static information flow checking to work even when trust relationships change over time.

Two principals are already built into Swift programs. The principal ( a.k.a.server) represents the maximally trusted

* principal in the system. The principal client represents the other end of the current session—in ordinary, nonmalicious use, a Web browser under the control of a user. When reasoning about security, we can only assume that the client is the other end of a network connection, possibly controlled by a malicious attacker. Because the server is trusted, the principal *

acts for client. The client may see information whose confidentiality is no greater than → client, and can produce information with integrity no greater than ← client.

Labels defined in terms of principals are a key feature of the DLM. Because labels keep track of whose security is being

3. WRItInG s WIft aPPLICatIons enforced, they are useful for systems such as Web applications, where principals need to cooperate despite mutual 3. 1. Labels and principals distrust. By expressing labels in terms of principals, the DLM Programming with Swift starts with a program written in the also enables connections between policies for information Jif programming language. ^{13, 15} A little background on Jif will flow (labels), policies for trust and authorization (acts-for therefore be helpful. relationships), and processes for authentication. These con-

In Jif programs, information security requirements are nections are all important for Swift. expressed using labels from the decentralized label model A Swift program may use and even create additional prin- (DLM). ¹⁴ A label is a set of policies expressed in terms of prin- cipals, for example, to represent different users of a Web cipals. For example, the confidentiality policy alice → bob application. For a user to log in as principal bob, server-side says that principal alice owns the labeled information but applicationcode marked as trusted by bob must authenticate permits principal bob to read it. Similarly, the integrity pol- the user, establishing that the principal named by client icy alice ← bob means that alice permits bob to affect acts for bob. Requests from that browser are then treated as the labeled information. coming from bob, and information readable by bob can be

Labels can be attached to types, making Jif a security- sent there. All this can be accomplished within the Jif pro- typed language. For example, the following declaration uses gramming model.

a label containing two policies separated by a semicolon:

2. 6. swift run-time system

In order to enforce the security requirements in the Jif source code, information flows between the client and the server must be strictly controlled. In particular, confidential information must not be sent to the client, and information received from the client cannot be trusted. The Swift compilation process generates code that satisfies these constraints. These constraints are also enforced by the Swift run-time system, which ensures that information coming from the client is never trusted.

int {alice → bob,alice; bob ← alice} y;

It means that the information in y is considered sensitive by alice, who wants to restrict its release only to bob and alice; and further that it is considered trustworthy by bob, who wants to permit only alice to affect it.

The Jif compiler uses labels to statically check that information flows within Jif code are secure. For example, consider the following code fragment (using the same variable y):

int{alice}→bob x = y

This code causes information to flow from y to x. For the code to be secure, the label on x must restrict the use of data in x at least as much as the label on y restricts the use of y. This is true

3. 2. sample application

The key features of the Swift programming model can be seen in a simple Swift Web application. Figure 2 shows fragments of the source code for the number-guessing Web application described in Section 1. Java programmers may recognize this Jif code as similar to that of an ordinary sin-gle-machine Java application with a user interface dynamically constructed out of widgets such as buttons, text inputs, and text labels. Swift widgets are similar to those in the GWT, ⁸ communicating via events and listeners. The key difference is that Swift controls how information flows through widgets.

The core application logic is found in the makeGuess method (lines 15–39). Other than security label annotations, this is essentially straight-line Java code. To implement the same functionality with technologies such as JSP² or GWT

febrUary 2009 | vol. 52 | no. 2 | CommunICatIons of the aCm

81