Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal modeling and automatic enforcement of Bring Your Own Device policies
Armando A., Costa G., Merlo A., Verderame L. International Journal of Information Security14 (2):123-140,2015.Type:Article
Date Reviewed: Jul 14 2015

The diffusion of personal, network-enabled, electronic devices is forcing organizations to consider the enforcement of bring your own device (BYOD) policies; this proves to be true also for organizations that do not support BYOD computing models at all due to security concerns. In some cases, policies could be as simple as making “off limits” all kinds of personal devices, while in other cases, access to enterprise applications could be granted, subject to security and management policies.

This paper discusses the automatic enforcement of BYOD policies, not only in an empirical manner, but also through the application of formal methods. The proposed framework covers the aspects related to the enforcement of security policy and the analysis of application behaviors, aiming at a transparent user experience, minimizing changes to operating system interfaces and workflow, and providing ways to ensure device safety in a fully automated way.

The policy specification is provided using Hennessy-Milner logic (HML) and applying partial model checking (PMC) to create a specialized security policy. A formal proof of validity is given, together with empirical evidence of the feasibility of the proposed approach, obtained through the testing of 261 Android applications available from Google Play. This paper is interesting mainly for the use of formal methods to analyze the system, to provide correspondence between system description and properties of interest, and to pave the road toward the efficient automation of security processes.

Reviewer:  Alessandro Berni Review #: CR143609 (1509-0798)
Bookmark and Share
  Featured Reviewer  
 
Formal Models Of Communication (E.4 ... )
 
 
Model Checking (D.2.4 ... )
 
 
Security and Protection (C.2.0 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Models Of Communication": Date
Statistical and inductive inference by minimum message length (Information Science & Statistics)
Wallace C., Springer-Verlag New York, Inc., Secaucus, NJ, 2005.  432, Type: Book (9780387237954)
Jan 17 2006
A different approach to finding the capacity of a Gaussian vector channel
Tsybakov B. Problems of Information Transmission 42(3): 183-196, 2006. Type: Article
Oct 15 2007
Stochastic recovery problem
Darkhovsky B. Problems of Information Transmission 44(4): 303-314, 2008. Type: Article
May 21 2009
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy