[Impressum] [Datenschutz] [E-Mail] [Back to the main project page]

Modeling the Travel Planner Application with IFlow

  1. The Application

  2. A Modeling Walkthrough

    1. Component Diagram

    2. Sequence Diagram

    3. Properties

    4. Policy

    5. Message Diagram

  3. The formel model with proofs

The Application

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).

A Modeling Walkthrough

Component Diagram

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.




Message Diagram

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.

Sequence Diagrams

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.

Overview

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.


Get Flight Offers

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.

Choose Flight

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".

Release Credit Card Details

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.

Book Flight

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.

Properties






Policy






The formal model with proofs

The formal specification is a web presentation of a KIV project. Green boxes denote specifications that are automatically generated from the UML model while orange boxes denote imported library specifications.

The proof of the unwinding condition and the information flow properties can be found in the Properties specification. The yellow theorems are axioms that specify the different policies. The purple ones at the bottom (and below) are the actual properties. In the specification you can click on the properties and see their proofs.