Movie Rental

This scenario demonstrates the use of security policies on databases. The database consists of a list

of items (e.g. movies) subject to events (e.g. movie rentals) happening at a certain location and time. The location of an event consists of latitude and longitude and it is confidential. Otherwise all other information is public. The policy is modelled as follows: the database policy assigns to the latitude and longitude a high security level. Leaks to the client are prevented by labelling the return values of RPC functions as public. The following LINQ query joins rentals with movies and returns a list of movie titles. Movie titles are input to an RPC function which is only allowed to return public values. As a result the first yield statement is allowed to return the movie title. If instead we use the second yield statement, JSLINQ will reject the program.

let events = query {

for e in db.Event do

for i in db.Item do

if e.ItemId = i.Id then

(* Allowed *) yield i.Name

(* Blocked *) yield (string e.Lat) }

Moreover, we allow the user to retrieve a ranking of movies that are popular within an area. The implementation contains a pre-defined set of areas which are addressed using indexes. The user is only allowed to specify the index for an area of interest. The application server filters the list of movie rentals based on the coordinate values. JSLINQ will infer a high security level for the length of the resulting list, as it depends on the secret coordinate values. Our policy allows that geographic information about rentals is disclosed on the granularity of fixed-size areas, therefore we can directly declassify the length of that list. The scenario consists of 87 F# and 6231 generated Javascript LOCs.