====== ObSec: Declassification policies using type abstraction ======

ObSec is a simple object-oriented language that supports type-based declassification. ObSec was introduced in the paper 
{{bib>cruzAl-ecoop2017|Type Abstraction for Relaxed Noninterference}}

This tutorial covers: 
  * how to install a web interpreter (ObSec Pad) for the ObSec language.
  * a basic presentation of the language syntax,
  * the type-based declassification examples that appear in the paper.


===== Installation instructions =====

We provide three ways to access to the ObSec Pad (although we strongly recommend the first one!):

  - **Using the online ObSec Pad** at [[https://pleiad.cl/obsec]]. 
  - **With the virtual machine**, which can be downloaded [[https://pleiad.cl/ecoop17-artifact.zip|here]]
  - **Local execution of the ObSec Pad**, which can be downloaded [[https://pleiad.cl/_media/research/software/obsec/obsec-web.zip|here]].

The **online ObSec Pad** does not require any installation and is always up-to-date. If you want to get a snapshot of the current state of the interpreter (as of April 18, 2017), then follow the instructions for points 2 or 3.

==== The virtual machine ====
We have set up a virtual machine with an Ubuntu installation and Java 1.8. The virtual machine image was created with Virtual Box 5.1.18.
  - Install Virtual Box 5.1.18 or higher.
  - Import the Virtual Machine Image
  - Start the Virtual Machine
  - Use the following credentials to log in: username: dev , password: qwe123
  - Open a terminal. (Make sure you are at home.)
  - Run <code bash>
./obsec-web/bin/obsec-web
</code>

This should start a server on port 9000. To open the ObSec Pad go to http://localhost:9000/obsec/


==== Local execution of the ObSec Pad ====

To run the ObSec Pad locally, all you need is Java 1.8. Also check that you have Java 1.8 in the path.

The following instructions are Unix valid commands. If you have Windows installed in your machine, you need to perform the corresponding commands.
  - Unzip the file.<code bash>
unzip obsec-web.zip
</code>
  - Go to the "obsec-web " folder:<code bash>
cd obsec-web
</code>
  - Add run permissions to the binary file:<code bash>
chmod +x bin/obsec-web
</code>
  - And then run:<code bash>
./bin/obsec-web
</code>This should start a server in the port 9000. To open the ObSec Pad, go to http://localhost:9000/obsec/
  - In case the port 9000 is already taken, run:<code bash>
./bin/obsec-web -Dhttp.port=<available-port-number>
</code>

===== ObSec Pad: Functionality=====
The following screenshot shows how the ObSec Pad looks like

{{:research:software:obsec:obsec-interpreter.png?600|}}

Note that even though we provide some predefined examples, we suggest you finish this tutorial first. It will help you understand the syntax of ObSec and how to define and use type-based declassification policies.

The ObSec Pad has the minimal functionality you expect for an interpreter:
  * Details of the language syntax. 
  * Type checking. It gives you the type of the program or an error if the program is not well-typed or if it has a syntax error.
  * Execution. If the program was well-typed (as the result of clicking "TYPECHECK!"), the interface will show a button to execute the program.


===== Introduction to ObSec : Warm up =====

ObSec is a minimal object-oriented language, which includes the following expressions: variables, object definitions, method invocations as well as built-in values. The implementation of ObSec also includes a number of convenient forms (not present in the formal core in the paper): integers, strings, boolean, string lists, as well as local variable definitions and type alias declarations. 

Example of valid programs in ObSec are:
<code>
1.+(2)
</code>
<code>
"qwe123".length()
</code>
<code>
if "qwe123".length().==(6) then 1 else 0
</code>
<code>
mklist("b","c","a")
</code>
<code>
let{
 val s = "qwe123"
 val l = s.length()
} in
if l.==(6) then 1 else 0
</code>

==== Types ====

The distinguishing feature of ObSec are security types: a security type ''S'' is a two-faceted type ''T<U'', where ''T'' (resp. ''U'') is the private (resp. public) facet. **However for the sake of presentation of the language syntax, the first examples will contain only types of the form ''T<T''. To write such types (where the private and public facet are equals), you can use either the syntax ''T<L'' or just ''T''**. 

ObSec includes predefined types ''Int'', ''String'', ''Bool'', and ''StrList'' lists of strings). You can see the type interface of built-in types in the Syntax Dialog in the ObSec Pad.

{{:research:software:obsec:syntax.png?400|}}

 You can define and use object types in different ways. Below, we illustrate this by creating an object type with a login method that takes two public strings and returns a public integer:
  * Inline structural type definition: the type is defined (anonymously) where it is used <code>
[{login: String String -> Int}]
</code>
  * Type alias declaration: gives a name (type alias) to an object type, convenient to reuse the same object type definition.<code>
type AuthServer  = [{login: String String -> Int}]
</code>
  * Type definition: this is just a syntactic sugar for a type alias declaration, which additionally allows the definition of //recursive// object types, as discussed in the following paragraph. <code> 
deftype AuthServer {
    {login: String String -> Int}
 }
</code> 

==== Recursive types ====
The convenient way to define recursive types in the implementation of ObSec is using the ''deftype'' keyword. For example, the following code snippet defines the type of binary trees of strings. Methods ''left'' and ''right'' use the defined type ''BinTree''.  
<code>
deftype BinTree{
    {isEmpty: -> Bool}
    {value: -> String}
    {left: -> BinTree}
    {right: -> BinTree}
}
</code>

The above code is equivalent to:
<code>
type BinTree = [X
    {isEmpty: -> Bool}
    {value: -> String}
    {left: -> X}
    {right: -> X}
]
</code>
where the type variable ''X'' represents the defined recursive type. This core syntax is the one adopted in the paper, but which is less convenient to use than ''deftype''.

==== Objects ====

ObSec does not have classes, instead one defines literal objects. An object is a collection of method definitions, where method names are unique. The object definition explicitly names the self variable (''z'' in the example below) and binds it in method bodies. The self variable is ascribed with the type of the object: ''AuthServer<L'' indicating that the created object is public. The object below just has a method ''login'' that receives two arguments: ''password'' and ''guess''. The type of the arguments are obtained from the ''login'' method signature in ''AuthServer''.

<code>
new {z : AuthServer<L => 
  def login password guess = if password.==(guess) then 1 else 0
}
</code>

Executable example:

<code>
let {
    type AuthServer = [{login : String String -> Int}]
    val auth = new {z : AuthServer<L => 
                 def login password guess = if password.==(guess) then 1 else 0
               }
} in 
auth.login("qwe123","qwe123")
</code>




==== Recursive methods ====
We now present an example with a recursive method definition. The following code shows how to use the self variable (''z'') to implement a recursive method ''contains'' over a list. The type of ''listHelper'' is defined in the type ascription of ''z'':
<code>
let {
  val listHelper =  new {z : [{contains : StrList<L -> Bool<L}] <L => 
                      def contains myList  = 
                       if myList.isEmpty() 
                       then false 
                       else 
                         if myList.head().==("a") 
                         then true 
                         else z.contains(myList.tail())
                   }
} 
in
listHelper.contains(mklist("b","c","a"))
</code>

Once you warm up with the examples, you can inspect the full syntax supported by the ObSec Pad. The syntax is essentially the one of the paper extended with built-in types and surface language constructions that makes programming more convenient.

=== Syntax ===
<code>
S	::=	T < T	                                                                                (Security types)
T	::=     Bool |Int |String | StrList | X | OT	                                                (Types)
OT	::=	[X M*] | [M*]	                                                                        (Object Type)
M	::=	{ name : S* -> S }	                                                                (Method signature)
t	::=	o | x | t.m(t) | b | n | s |if t then t else t | mkList(t*) | let { TD* TA* VD* } in t	(Terms)
o	::=	new { x : S => (def name x* = t)* }	                                                (Object)
TD	::=	deftype{ M* }	                                                                        (Type Declaration)
TA	::=	type X = OT	                                                                        (Type Alias)
VD	::=	val x = t	                                                                        (Value declaration)
b	::=	true | false	                                                                        (Booleans)
n	::=	natural numbers	                                                                        (Natural numbers)
s	::=	string literals	                                                                        (String literals)
X	::=	identifier	                                                                        (Type Variable)
</code>
You also can access the syntax definition in the ObSec Pad. 

==== Security Typing in ObSec ====

The distinguishing feature of ObSec are security types ''T<U'', where ''T'' (resp. ''U'') is the private (resp. public) facet. For instance the type ''String<H'' (a shortcut to ''String<[]'') represents to a private string, while ''String<L'' (a shortcut to ''String<String'' represents a public string. Note that for a security type ''T<U'' to be well-formed, T must be a subtype of U.

In other words, the empty interface type (the root of the subtyping hierarchy) denotes an object that hides all
its attributes, which intuitively coincides with secret data, while the interface that coincides with the implementation type of an object exposes all of them, which coincides with public data.

The following example changes the type of the ''password'' argument in method ''login'' signature to ''String<[]'' making the ''password'' argument secret.

<code>
let{
    type AuthServer = [{login : String<[] String -> Int<L}]
    val auth = new {z : AuthServer<L => 
                 def login password guess = if password.==(guess) then 1 else 0
               }
} in 
auth.login("qwe123","qwe123")
</code>

This program is not well-typed because the implementation of the login method is using the ''=='' method, which is not available in the public facet. Hence the conditional expression ''password.==(guess)'' has type ''Bool<H'' and the whole ''if'' expression has type ''Int<H'', which is not a subtype of ''Int<L''. (As you can expect, ''T1<U1'' is a subtype of ''T2<U2'' if ''T1'' is a subtype of ''U1'' and ''T2'' is a subtype if ''U2''). The ObSec type checker rejects this program to prevent an invalid information flow (from the secret password to a public result).


==== Declassification Policies in ObSec ====

As explained in the Sections "Introduction" and "Type-Based Declassification Policies" of the paper, in some scenarios, programs need to declassify //some// information about secrets as part of their functionality (as in the password checking algorithm). 

Our main observation is that any interface between the empty type and the implementation type denotes
declassification opportunities, and hence we can provide a //controlled// declassification approach.

For example we can just expose the ''=='' method for the ''password'' by including it in the public facet of the argument type.

<code>
let{
  type StringEq = [{== : String -> Bool}]
  type AuthServer = [{login : String<StringEq String -> Int<L}]
  val auth = new {z : AuthServer<L => 
               def login password guess = if password.==(guess) then 1 else 0
             }
} in 
auth.login("qwe123","qwe123")
</code>
Now the program is well typed and we have a guarantee that only the ''=='' method of the ''password'' argument is invoked. 

For instance, try to change the condition in the ''if'' to ''password.hash().==(guess.hash())''. The resulting program is not well-typed, because ''hash'' is not in the public facet of the ''password'' security type.

=== Progressive declassification policies ===
Declassification can be progressive, requiring several operations to be performed in order to obtain public data. For instance, 
"the result of comparing the hash of the password for equality can be made public". This policy can be expressed with the type:

<code>
type StringHashEq = [{hash : -> Int<[{== : Int -> Bool}]}]
</code>
The implementation of the login method now adheres to the ''password'' policy and then the program is well typed.
<code>
let{
  type StringHashEq = [{hash : -> Int<[{== : Int -> Bool}]}]
  type AuthServer = [{login : String<StringHashEq String -> Int<L}]
  val auth = new {z : AuthServer<L => 
               def login password guess = if password.hash().==(guess.hash()) then 1 else 0
             }
} in 
auth.login("qwe123","qwe123")
</code>

Variations to the above program that do not respect the policy and hence are not well-typed:
  * Change the conditional expression to password.hash().+(1).==(guess.hash().+(1)). 
  * Change the conditional expression to password.length().==(guess.length()).


=== Recursive declassification ===
Recursive declassification policies are desirable to express interesting declassification of either inductive data structures or object interfaces (whose essence are recursive types). Consider for instance a secret list of strings, for which we want to allow traversal of the structure and comparison of its elements with a given string. This can be captured by the recursive type ''StrEqList'' defined as:

<code>
deftype StrEqList{
  {isEmpty: -> Bool<L}
  {head: -> String<StringEq}
  {tail: -> StrList<StrEqList}                                
}
</code>

To allow traversal, the declassification policy exposes the methods ''isEmpty'', ''head'' and ''tail'',
with the specific constraints that a) accessing an element through ''head'' yields a ''StringEq'' (not
a full ''String'') and b) the ''tail'' method returns the tail of the list with the same declassification
policy ''StrEqList''. 

The following program shows an implementation of a ''contains'' method over a list with the declassification policy ''StrEqList''

<code>
let{
  type StringEq = [{== : String -> Bool}]
  deftype StrEqList{
    {isEmpty: -> Bool<L}
    {head: -> String<StringEq }
    {tail: -> StrList<StrEqList}
  }
  val listHelper =  new {z : [{contains : StrList<StrEqList -> Bool<L}]<L  =>
                      def contains myList  =
                        if myList.isEmpty()
                        then false
                        else
                          if myList.head().==("a")
                          then true
                          else z.contains(myList.tail())
                    }
}
in
listHelper.contains(mklist("b","c","a"))
</code>

Any method invocation over the ''head'' of the list (different than ''=='')  renders the program ill-typed. For instance, changing the inner ''if'' condition to ''myList.head().hash().==("a".hash())'': the type checker reports "Both branches of an if expression must have the same type". This is because the ''else'' branch of the outer ''if'' has type ''Bool<H'' while the ''then'' branch has type ''Bool<L''.



=== Simple Case of Study: Web App with Payment System ===
The following program illustrates a more elaborated example where different declassification policies are used in an application that processes user payments. 
The application has 4 modules:
  * ''Controller''. It manages the user requests to pay the "television".
  * ''View''. It models the application web page and contains a method ''show'' to "display" a message in the application web page. The method ''show'' models the public channel in the application.
  * ''PaymentGateWay''. It models a payment gateway with the method ''pay'' that receives the user name, her credit card and the service that she wants to pay. ''PaymentGateWay'' is a trusted component that can use the internal representation of a ''CreditCard''. We return just ''true'' as the implementation of the ''pay'' method. Since ObSec does not model “trusted declassification” (//Hicks et al. [2006]//), we cannot give a proper implementation for the method ''pay''. This limitation is discussed in the paper (section "Expressiveness of Declassification Policies", paragraph "More advanced scenarios").
  * ''UserManager''. It contains two methods: ''verifyCredentials'' and ''getUserCreditCard''. The ''UserManager'' instance uses an internal backend (of type ''Backend''). The backend instance contains the sensible information. It has a method ''findUser'' that returns the user with the ''UserPolicy'' type as the public facet. The ''UserPolicy'' type reuses the policies ''StringHashEq'' and ''CCPolicy'' to restrict the return type of the methods ''password'' and ''creditCard'' of ''User'' type respectively. The ''CCPolicy'' type exposes the last four digits of a credit card. The signature for the method ''getUserCreditCard'' also uses this declassification policy (''CCPolicy''). The method ''verifyCredentials'' returns a boolean value indicating if the supplied credentials "are in" the backend. It adheres to the password policy (StringHashEq) in its implementation.

The types ''PaymentGateWay'', ''Backend'' and ''View'' have "toy" implementations because the ObSec language is just a "proof-of-concept" language and it does not include all the necessary features for a proper implementation of these types.

The implementation of the method ''payInternet'' in the ''Controller'' instance (''controller'') orchestrates the payment process. First it verifies the credential of the user, then it uses the payment gateway to pay the service. If the payment is successful, the ''payInternet'' method uses the ''View'' instance to show the last four digits of the credit card. The method ''last4Digits'' is in the declassification policy (''CCPolicy'') of the user credit card and its result is public. It means that method call ''view.show(cc.last4Digits())'' is valid.

<code>
let{
  type StringHashEq = [{hash : -> Int<[{== : Int -> Bool}]}]
  type CCPolicy = [{last4Digits: -> String}]
  
  type CreditCard = [{number: -> String}
                     {securityNumber: -> String}
                     {last4Digits: -> String}]
                     
  type UserPolicy = [{name: ->String}
                     {password: -> String<StringHashEq}
                     {creditCard: -> CreditCard<CCPolicy}]
  type User = [{name: ->String}
               {password: -> String}
               {creditCard: -> CreditCard<CCPolicy}]
 
  
                     
  
  type Controller = [{payInternet: String String -> String}]
  type View = [{show : String -> String}]
  type PaymentGateWay = [{pay: String CreditCard<[] String -> Bool}]
  
  type UserManager = [{verifyCredentials: String String -> Bool}
                      {getUserCreditCard: String -> CreditCard<CCPolicy}]
  
  val paymentGateWay =  new {pg:PaymentGateWay =>
                          def pay user cc service  = true
                        }
  val userManager = let{
                      type Backend = [{findUser: String -> User<UserPolicy}]
                      val backend = new {b:Backend =>
                                        def findUser login = 
                                            new {u:User =>
                                              def name = login
                                              def password = "qwe123"
                                              def creditCard = 
                                                new {cc : CreditCard =>
                                                  def number = "5500-0000-0000-0004"
                                                  def securityNumber = "678"
                                                  def last4Digits = "0004"
                                                }
                                        }
                                    }
                      
                    } in 
                    new {z:UserManager =>
                      def verifyCredentials login password = 
                        let{
                          val dbUser = backend.findUser(login)
                        }
                        in 
                          if dbUser.password().hash().==(password.hash()) 
                          then true
                          else false
                          
                      def getUserCreditCard login = backend.findUser(login).creditCard()
                    }
  
  val view =  new {v:View =>
                def show s = s
              }
  val controller = new {z : Controller =>
                      def payInternet loginFromWeb  passFromWeb =
                    		if userManager.verifyCredentials(loginFromWeb,passFromWeb)
                    		then
                    		  let{
                    		    val cc = userManager.getUserCreditCard(loginFromWeb)  
                    		  } 
                    		  in
                      			if paymentGateWay.pay(loginFromWeb,cc,"television")
                      			then
                      				view.show(cc.last4Digits())
                      			else
                      				view.show("Oops. We are unable to process your payment now")
                    		else
                    		  view.show("Oops. Invalid credentials!")
                    }
}
in 
controller.payInternet("john","qwe123")
</code>

Variations to the above program that do not respect the policies and hence are not well-typed:
  * change the expression ''view.show(cc.last4Digits())'' to ''view.show(cc.number())''. The ''number'' method is not in the public policy of a credit card object (returned by a ''UserManager''). 
  * remove the method ''last4Digits'' from ''type CCPolicy = [{last4Digits: -> String}]''
  * change the signature of the method ''getUserCreditCard'' in the ''UserManager'' type to: ''{getUserCreditCard: String -> CreditCard}''