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:01] 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 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 312: Line 312:
  
  
-=== Basic Case of Study: Web App with Payment System ===+=== 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 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: The application has 4 modules:
   * ''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>
Line 408: Line 408:
  
 Variations to the above program that do not respect the policies and hence are not well-typed: 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'').  +  * 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 method ''last4Digits'' from ''type CCPolicy = [{last4Digits: -> String}]'' +  * remove the method ''last4Digits'' from ''type CCPolicy = [{last4Digits: -> String}]'' 
-  * change the signature of method ''getUserCreditCard'' in ''UserManager'' type to: ''{getUserCreditCard: String -> CreditCard}''+  * change the signature of the method ''getUserCreditCard'' in the ''UserManager'' type to: ''{getUserCreditCard: String -> CreditCard}''