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
Last revisionBoth sides next revision
research:software:obsec [2017/04/27 01:17] racruzresearch:software:obsec [2017/05/18 00:52] racruz
Line 5: Line 5:
  
 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 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 317: Line 317:
   * ''Controller''. It manages the user requests to pay the "television".   * ''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.   * ''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 "trueas 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"). +  * ''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 policy for a user. The ''UserPolicy'' type reuses the policies ''StringHashEq'' and ''CCPolicy'' to restrict access to the methods ''password'' and ''creditCard'' of ''User''. The ''CCPolicy'' type exposes the last four digits of a credit card. The credit cards returned by the ''getUserCreditCard'' method 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.+  * ''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 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. It 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.+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> <code>