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