TY - GEN
T1 - Types for Location and Data Security in Cloud Environments
AU - Gazeau, Ivan
AU - Chothia, Tom
AU - Duggan, Dominic
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/9/25
Y1 - 2017/9/25
N2 - Cloud service providers are often trusted to be genuine, the damage caused by being discovered to be attacking their own customers outweighs any benefits such attacks could reap. On the other hand, it is expected that some cloud service users may be actively malicious. In such an open system, each location may run code which has been developed independently of other locations (and which may be secret). In this paper, we present a typed language which ensures that the access restrictions put on data on a particular device will be observed by all other devices running typed code. Untyped, compromised devices can still interact with typed devices without being able to violate the policies, except in the case when a policy directly places trust in untyped locations. Importantly, our type system does not need a middleware layer or all users to register with a preexisting PKI, and it allows for devices to dynamically create new identities. The confidentiality property guaranteed by the language is defined for any kind of intruder: we consider labeled bisimilarity i.e. an attacker cannot distinguish two scenarios that differ by the change of a protected value. This shows our main result that, for a device that runs well typed code and only places trust in other well typed devices, programming errors cannot cause a data leakage.
AB - Cloud service providers are often trusted to be genuine, the damage caused by being discovered to be attacking their own customers outweighs any benefits such attacks could reap. On the other hand, it is expected that some cloud service users may be actively malicious. In such an open system, each location may run code which has been developed independently of other locations (and which may be secret). In this paper, we present a typed language which ensures that the access restrictions put on data on a particular device will be observed by all other devices running typed code. Untyped, compromised devices can still interact with typed devices without being able to violate the policies, except in the case when a policy directly places trust in untyped locations. Importantly, our type system does not need a middleware layer or all users to register with a preexisting PKI, and it allows for devices to dynamically create new identities. The confidentiality property guaranteed by the language is defined for any kind of intruder: we consider labeled bisimilarity i.e. an attacker cannot distinguish two scenarios that differ by the change of a protected value. This shows our main result that, for a device that runs well typed code and only places trust in other well typed devices, programming errors cannot cause a data leakage.
UR - http://www.scopus.com/inward/record.url?scp=85033783873&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85033783873&partnerID=8YFLogxK
U2 - 10.1109/CSF.2017.25
DO - 10.1109/CSF.2017.25
M3 - Conference contribution
AN - SCOPUS:85033783873
T3 - Proceedings - IEEE Computer Security Foundations Symposium
SP - 376
EP - 391
BT - Proceedings - IEEE 30th Computer Security Foundations Symposium, CSF 2017
T2 - 30th IEEE Computer Security Foundations Symposium, CSF 2017
Y2 - 21 August 2017 through 25 August 2017
ER -