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).
8 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).
14 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,
8 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 JSP2 or GWT
febrUary 2009 | vol. 52 | no. 2 | CommunICatIons of the aCm
81