A conservative algorithm for computing the flow of permissions in Java programs
- 1 July 2002
- proceedings article
- Published by Association for Computing Machinery (ACM) in ACM SIGSOFT Software Engineering Notes
- Vol. 27 (4) , 33-43
- https://doi.org/10.1145/566172.566178
Abstract
Open distributed systems are becoming increasingly popular. Such systems include components that may be obtained from a number of different sources. For example, Java allows run-time loading of software components residing on remote machines. One unfortunate side-effect of this openness is the possibility that "hostile" software components may compromise the security of both the program and the system on which it runs. Java offers a built-in security mechanism, using which programmers can give permissions to distributed components and check these permissions at run-time. This security model is flexible, but using it is not straightforward, which may lead to insufficiently tight permission checking and therefore breaches of security.In this paper, we propose a data flow algorithm for automated analysis of the flow of permissions in Java programs. Our algorithm produces, for a given instruction in the program, a set of permissions that are checked on all possible executions up to this instruction. This information can be used in program understanding tools or directly for checking properties that assert what permissions must always be checked before access to certain functionality is allowed. The worst-case complexity of our algorithm is low-order polynomial in the number of program statements and permission types, while comparable previous approaches have exponential costs.Keywords
This publication has 22 references indexed in Scilit:
- A formal specification of Java class loadingACM SIGPLAN Notices, 2000
- Tool support for planning the restructuring of data abstractions in large systemsIEEE Transactions on Software Engineering, 1998
- Improving efficiency of symbolic model checking for state-based system requirementsPublished by Association for Computing Machinery (ACM) ,1998
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- The security of static typing with dynamic linkingPublished by Association for Computing Machinery (ACM) ,1997
- Evaluating deadlock detection methods for concurrent softwareIEEE Transactions on Software Engineering, 1996
- Data flow analysis for verifying properties of concurrent programsPublished by Association for Computing Machinery (ACM) ,1994
- Interprocedural static analysis of sequencing constraintsACM Transactions on Software Engineering and Methodology, 1992
- Pointer-induced aliasing: a problem taxonomyPublished by Association for Computing Machinery (ACM) ,1991
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986