The information flow (IF) policy is then modeled by annotating class associations with information flow security domains. An IFlow security domain is represented with a set of agents able to read the annotated data.
A starting example for an information flow
sensitive information is a (simplified) travel planning application
for a smart phone. This is a realistic example since such
applications exist, and in the past smart phone applications have
been known to upload private data to some internet servers.
The
idea is to download the application from an App store. It allows to
book a flight and a hotel, e.g. to visit a conference. The program is
sponsored and developed by a travel agency that acts as a broker for
the airline and the hotel. The application uses dedicated web
services to find flights and hotels online. It checks the user's
personal calendar (either on the phone or online) to find out if it
is possible to fly a day earlier or return a day later than planned,
and fixes the final dates in the calendar. In order to pay, the
user's credit card details, which are stored inside a credit card
center application on the mobile device, are accessed.
So
we have different parties (the user, the travel agency, different
airlines, and different hotels) that should be given only the minimal
necessary informations. For example: payment info is sent only to the
chosen airline and hotel after explicit confirmation by the user.
Calendar details (except the possible travel dates) are never sent to
anybody. Arrival and departure dates are sent to the hotels, but no
other flight details. The travel agency gets the information which
airline and hotel was chosen (to collect fees), but no personal
information about the user. And so on. Clearly, this application is
concerned with information flow in a non-trivial manner, because some
secret information must be made partially public.
The idea is
to model (part of) the application with UML. We use a class diagram
to model the static part of the application and sequence diagrams
that describe the usage of the application. The developer can also
model information flow policies. Based on these annotations,
information flow properties (typically noninterference modulo some
declassification) are expressed.
The model is transformed
automatically into code skeletons and annotations for a programming
framework that supports information flow control, e.g. Jif or Joana.
The skeleton parts must be implemented by the developer obeying
certain programming guidelines (e.g., no usage of declassification
statements). The idea is that if the full program type checks it
comforms to the information flow policies described in the abstract
model. For deployment, the properties of the developed application
can be certified by a trusted third party, e.g. in an App store
setting, or could be ensured by proof carrying code.
A
step-by-step modeling walkthrough for a simple version of the
Travel Planner application (without hotel booking or a calendar
application) can be found below. Its security annotations capture the
security property "the travel agency never learns the user's
credit card details".
The Java code can be downloaded here (PDG, analyzable with JOANA).
We start off by specifying all application agents and
necessary data types using a UML class diagram. Agents are marked
with the stereotypes "User", "Application", or
"Service" from the IFLow UML profile denoting a class as a
representation of a user, a mobile application, or a web
service. Class operations can be used in sequence diagrams. Their
method bodies have to be implemented by hand.
The information
flow (IF) policy is then modeled by annotating class associations
with information flow security domains. An IFlow security domain is
represented with a set of agents able to read the annotated data.
Another class diagram is used to model messages sent between
agents by inheriting from an abstract class marked with the
stereotype "Message". Their attributes and associations
denote the data inside such mesages. Class constructors denote the
order of attributes and associations, which is necessary for the
sequence diagrams.
Messages
sent to and from a user are standardized, as they represent alert-,
input- and confirmation-UI-elements on a smart phone. They are part
of the provided IFlow UML package.
The IFlow approach uses sequence diagrams to model the communication between agents, leaving out implementation details of local functionality. The sequence diagrams denote the message sequences between agents of the Travel Planner application. Since "combined fragments" have been introduced in UML 2.0, one sequence diagram can specify several traces of program execution. We use a variation of the Model Extension Language (MEL) to denote message instantiations, procedure calls and variable assignments. Messages are annotated with security levels denoting the upper bound for the confidentiality of sent data; it is thus not possible to send data annotated with "{User}" via a message annotated with "{User, Airline}" without prior declassification.
The sequence diagram below provides an overview over the dynamic
Travel Planner functionality and serves as a starting point for the
agent communication. We model messages and their replies with UML
"synchCall" and "reply" elements. Their names
match the message class names from the message diagrams. The sent
data is modeled as parenthesized arguments of those messages, which
must correspond to the attributes of the message class.
The first step of booking a trip is getting flight offers from a
travel agency. In the diagram above, the user is asked to input his
flight request (e.g., containing the travel date and the desired
price point) by sending him the "GetInput<RequestData>"
message (the desired type of input is stated within arrow brackets).
The user's input is captured with his "input" attribute,
which is returned and renamed to "requestData" when the
answer is received by the TravelPlanner app. This data is forwarded
to an airline via the travel agency and used to select relevant
flight offers using the manual function "filterOffers(..)".
The list of such offers is then returned to the TravelPlanner
app.
Each message is annotated with "{User, TravelAgency,
Airline}"; thus, only public information such as the airline's
flight offers can be sent via those messages.
The user now has to select a desired flight offer from the filtered list of offers returned by the airline. This is done by sending him the "GetSingleSelection" message containing the offers, to which he replies with a "BookSelected" message containing a selected offer stored in his attribute "singleSelection".
The user has now selected a desired flight offer and is about to
book his flight. To do so, the airline needs payment information
stored in the CreditCardCenter app; the user thus needs to be
informed that sensitive information is about to leave the phone.
In
the diagram below, the user is notified, which information is about
to be released for which agent using the "ConfirmRelease"
message. After a successful confirmation, a copy of his or her credit
card details is declassified to the security level "{User,
Airline}" in order to be sent to and read by the airline.
If the credit card details were successfully declassified, the
travel planner app can now send them and the selected flight offer id
to the airline. The airline processes the booking, and can then pay a
commission to the travel agency.
The security level
annotations forbid that the airline communicates the credit card
details to the travel agency even after receiving them from the
travel planner app.
