Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
research:software:obsec [2017/04/25 18:52] – racruzresearch:software:obsec [2017/05/18 03: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 14: Line 14:
 We provide three ways to access to the ObSec Pad (although we strongly recommend the first one!): 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/|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: Funtionalities=====+===== 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 (because the execution of the "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}''