figure 2: Guess-a-number Web application.

The makeGuess method receives a guess num from the client. The variable num is untrusted and not secret, as shown by its label { →client} on line 15. The label after

*

the method name, also { →client}, is the begin label of

*

the method. It controls information flows created by the fact that the method was invoked.

The code of makeGuess checks whether the guess is correct, and either informs the user that he has won, or else decrements the remaining allowed guesses and repeats. Because the guess is untrusted, Jif will prevent it from affecting trusted variables such as tries, unless it is explicitly endorsed by trusted code. Therefore, lines 21–37 have a checked endorsement that succeeds only if num contains an integer between 1 and 10. If the check succeeds, the number i is treated as a high-integrity value within the “then” clause. If the check fails, the value of i is not endorsed, and the “else” clause is executed. Checked endorsements are a Swift-specific extension to Jif that makes validating untrusted inputs both explicit and convenient.

Forcing the programmer to use endorse exposes a potential security vulnerability. In this case, the endorsement of i is reasonable because it is intrinsically part of the game that the client is allowed to pick any value in range.

Similarly, some information about the secret value secret is released when the client is notified whether the guess i is equal to secret. Therefore, the bodies of both the consequent and the alternative of the if test on line 23 must use an explicit declassify to indicate that information transmitted by the control flow of the program may be released to the client. Without the declassify, client-visible events—showing messages or updating the variable tries—would be rejected by the compiler.

The declassify and endorse operations are inherently dangerous. Jif controls the use of declassify and endorse by requiring that they occur in a code marked as trusted by the affected principals; hence the clauses authority ( ) and endorse ({ ← }) on line 16. The

*

latter, auto-endorse annotation means that an invocation of makeGuess is treated as trusted even if it comes from the client. Jif also requires integrity to perform declassification, enforcing robust declassification : untrusted

4

information cannot even affect security-critical release of information.

requires more code, in a less natural programming style with explicit control transfers between the client and server.

The code contains various labels expressing security
requirements; for simplicity, only the principals client 3. 3. swift user interface framework
and are used in these labels. For example, on line 3, the Swift programs interact with the user via a user interface
*
variable secret is declared to be completely secret ( → ) framework that abstracts away the details of the underly-
**
and completely trusted ( ← ); the variable tries on the ing HTML and JavaScript. Swift programming has a event-
**
next line is not secret ( →client) but is just as trusted. driven style familiar to users of UI frameworks such as
*
Because Jif checks transitively how information flows within Swing.
the application, the act of writing just these two label anno- To allow precise compile-time reasoning about informa-
tations constrains many other label annotations in the pro- tion flows within the user interface framework, all frame-
gram. The compiler ensures that all label annotations are work classes are annotated with security policies that track
consistent with the information flows in the program. information flow that may occur within the framework. The

The user submits a guess by clicking the button. A lis- framework ensures that the client is permitted to view all tener attached to the button passes the guess at line 50 to information that the user interface displays. Conversely, all makeGuess. The listener reads the guess from a Number information received from the user interface is annotated as TextBox widget that only allows numbers to be entered. having been tainted by the client.

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