Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
research:software:obsec [2017/04/25 17:45]
racruz
research:software:obsec [2017/05/18 00:54] (current)
racruz
Line 2: Line 2:
  
 ObSec is a simple object-oriented language that supports type-based declassification. ObSec was introduced in the paper  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}} ​to be presented at [[http://​conf.researchr.org/​home/​ecoop-2017|ECOOP 2017]] ​+{{bib>​cruzAl-ecoop2017|Type Abstraction for Relaxed Noninterference}}
  
 This tutorial covers: ​ This tutorial covers: ​
-  * how to install a web interpreter (ObSec Pad) for the ObSec language +  * how to install a web interpreter (ObSec Pad) for the ObSec language. 
-  * a basic presentation of the language syntax +  * a basic presentation of the language syntax, 
-  * the type-based declassification examples that appears ​in the paper.+  * the type-based declassification examples that appear ​in the paper.
  
  
Line 15: Line 15:
  
   - **Using the online ObSec Pad** at [[https://​pleiad.cl/​obsec]]. ​   - **Using the online ObSec Pad** at [[https://​pleiad.cl/​obsec]]. ​
-  - **With the virtual machine**, which can be downloaded [[https://​pleiad.cl/​paper_53_ubuntu_vm_obsec.ova|here]]+  - **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]].   - **Local execution of the ObSec Pad**, which can be downloaded [[https://​pleiad.cl/​_media/​research/​software/​obsec/​obsec-web.zip|here]].
  
Line 55: Line 55:
 </​code>​ </​code>​
  
-===== ObSec Pad: Funtionality=====+===== ObSec Pad: Functionality=====
 The following screenshot shows how the ObSec Pad looks like The following screenshot shows how the ObSec Pad looks like
  
Line 65: Line 65:
   * Details of the language syntax. ​   * 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.   * 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 ​it.+  * Execution. If the program was well-typed (as the result of clicking "​TYPECHECK!"​),​ the interface will show a button to execute ​the program.
  
  
Line 101: Line 101:
 {{:​research:​software:​obsec:​syntax.png?​400|}} {{:​research:​software:​obsec:​syntax.png?​400|}}
  
- You can define and use object types in different ways. Below, we illustrate by creating an object type with a login method that takes two public strings and returns a public integer:+ 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>​   * Inline structural type definition: the type is defined (anonymously) where it is used <​code>​
 [{login: String String -> Int}] [{login: String String -> Int}]
Line 309: Line 309:
  
 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''​. 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}''​