Università degli Studi di Foggia
In this paper, the authors describe a technique for guaranteeing that devices comply with a security policy. To do that, they use a type and effect system to infer behavioural models from applications implementation and they validate them against policy specification. Moreover, they define a novel approach, based on partial model checking, for partially evaluating the security policy depending on devices configurations. Finally, they present a prototype under implementation, called BYODroid, which concretely applies these techniques to secure the devices joining a virtual organisation in the BYOD style.