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/27 01:17]
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 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 "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"​). +  * ''​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>​