Article

Requirement enforcement by transformation automata

Author:

Douglas R. SmithAuthors Info & Claims

FOAL '07: Proceedings of the 6th workshop on Foundations of aspect-oriented languages

Pages 5 - 14

https://doi.org/10.1145/1233833.1233835

Published: 13 March 2007 Publication History

Abstract

The goal of this work is to treat safety and security policies as requirements to be composed in an aspectual style with a developing application. Policies can be expressed either logically or by means of automata. We introduce the concept of transformation automaton, which is an automaton whose transitions are labeled with program transformations. A transformation automaton is applied to a target program by a sound static analysis procedure. The effect is to perform a global transformation that enforces the specified policy. The semantic effect of this global transformation is explored.

In previous work we discussed how the intent of an AspectJ-style aspect can be expressed precisely and abstractly as a state invariant. Here, this result is generalized to handle invariants that are conditional and stated over both events and state properties. A policy stated in such a logical format can be translated to a transformation automaton that enforces it in a target program. The translation process is defined by a collection of inference schemes that can be mechanically instantiated and then solved, at least partially automatically, by deductive calculations.

References

[1]

Allan, C., Avgustinov, P., Christensen, A. S., Hendren, L. J., Kuzins, S., Lhotk, O., de Moor, O., Sereni, D., Sittampalam, G., and Tibble, J. Adding trace matching with free variables to AspectJ. In Proceedings of OOPSLA (2005), pp. 345--3640.

Digital Library

[2]

Brat, G., and Venet, A. Precise and scalable static program analysis of NASA flight software. In Proceedings of the 2005 IEEE Aerospace Conference (2005).

[3]

Cohen, D., Feather, M. S., Narayanaswamy, K., and Fickas, S. S. Automatic monitoring of software requirements. In ICSE '97: Proceedings of the 19th international conference on Software engineering (1997), ACM Press, pp. 602--603.

Digital Library

[4]

Colcombet, T., and Fradet, P. Enforcing trace properties by program transformation. In Proc. 27th ACM Symp. on Principles of Programming Languages (Jan. 2000), pp. 54--66.

Digital Library

[5]

Cousot, P., and Cousot, R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1977), ACM, pp. 238--252.

Digital Library

[6]

Dijkstra, E. W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, 1976.

Digital Library

[7]

Erlingsson, U., and Schneider, F. SASI enforcement of security policies: A retrospective. In Proceedings of the New Security Paradigms Workshop (Ontario, Canada, September 1999).

Digital Library

[8]

Ferraiolo, D., and Kuhn, D. Role based access control. In 15th National Computer Security Conference (1992).

[9]

Havelund, K., and Rosu, G. Monitoring Java programs with Java PathExplorer. In Electronic Notes in Theoretical Computer Science (2001), K. Havelund and G. Rosu, Eds., vol. 55, Elsevier.

[10]

Kiczales, G., and et al. An Overview of AspectJ. In Proc. ECOOP, LNCS 2072, Springer-Verlag (2001), pp. 327--353.

Digital Library

[11]

Lampson, B. W. Protection and access control in operating systems. Operating Systems, Infotech State of the Art Report 14 (1972), 309--326.

[12]

Manna, Z., and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, 1992.

Digital Library

[13]

Martinand, M., Livshits, B., and Lam, M. Finding application errors and security flaws using pql: a program query language. In OOPSLA '05: Proceedings of the 20th annual ACM SIGPLAN conference on Object Oriented Programming Systems Languages and Applications (2005), ACM Press.

Digital Library

[14]

Paige, R., and Koenig, S. Finite differencing of computable expressions. ACM Transactions on Programming Languages and Systems 4, 3 (July 1982), 402--454.

Digital Library

[15]

Pavlovic, D., and Smith, D. R. Composition and refinement of behavioral specifications. In Proceedings of Sixteenth International Conference on Automated Software Engineering (2001), IEEE Computer Society Press, pp. 157--165.

Digital Library

[16]

Poppleton, M., and Banach, R. Retrenchment: Extending the reach of refinement. In Proceedings of the Fourteenth Automated Software Engineering Conference (1999), IEEE Computer Society Press, pp. 158--165.

Digital Library

[17]

Reasoning Systems, Palo Alto, CA. The REFINE#8482; User's Guide, 1985.

[18]

Reps, T., Horwitz, S., and Sagiv, M. Precise interprocedural dataflow analysis via graph reachability. In Conference Record of the Twenty-Second ACM Symposium on Principles of Programming Languages (1995), ACM, pp. 49--61.

Digital Library

[19]

Schneider, F. Enforceable security policies. ACM Transactions on Information and System Security 3, 1 (February 2000), 30--50.

Digital Library

[20]

Smith, D. R. KIDS -- a semi-automatic program development system. IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering 16, 9 (1990), 1024--1043.

Digital Library

[21]

Smith, D. R. Mechanizing the development of software. In Calculational System Design, Proceedings of the NATO Advanced Study Institute, M. Broy and R. Steinbrueggen, Eds. IOS Press, Amsterdam, 1999, pp. 251--292.

[22]

Smith, D. R. Aspects as invariants. In Automatic Program Development: a Tribute to Robert Paige (2006), O. Danvy, F. Henglein, H. Mairson, and A. Pettorosi, Eds., Springer-Verlag LNCS. (earlier version in Proceedings of GPCE-04, LNCS 3286, 39--54).

[23]

Smith, D. R., and Havelund, K. Automatic enforcement of error-handling policies. Tech. rep., Kestrel Technology, September 2004.

[24]

Smith, D. R., and Havelund, K. Enforcing safety and security policies. Tech. rep., Kestrel Technology, December 2005.

[25]

Vanderperren, W., Suvee, D., Cibran, M., and de Fraine, B. Stateful aspects in JAsCo. In Proceedings of SC 2005 (2005), Springer-Verlag LNCS.

Digital Library

[26]

Vigna, G., and Kemmerer, R. NetSTAT: A Network-based Intrusion Detection System. Journal of Computer Security 7, 1 (1999), 37--71.

Digital Library

[27]

Walker, R., and Viggers, K. Implementing protocols via declarative event patterns. In SIGSOFT Foundations of Software Engineering (FSE04) (2004), ACM Press, pp. 159--169.

Digital Library

Cited By

Ebnenasir A(2015)Incremental Realization of Safety Requirements: Non-determinism vs. ModularityFundamentals of Software Engineering10.1007/978-3-319-24644-4_11(159-175)Online publication date: 12-Nov-2015
https://doi.org/10.1007/978-3-319-24644-4_11
Gorbovitski MLiu YStoller SRothamel TKiselyov OThompson S(2012)Composing transformations for instrumentation and optimizationProceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation10.1145/2103746.2103759(53-62)Online publication date: 23-Jan-2012
https://dl.acm.org/doi/10.1145/2103746.2103759
Liu YGorbovitski MStoller S(2009)A language and framework for invariant-driven transformationsACM SIGPLAN Notices10.1145/1837852.162161745:2(55-64)Online publication date: 4-Oct-2009
https://dl.acm.org/doi/10.1145/1837852.1621617
Show More Cited By

Index Terms

Requirement enforcement by transformation automata
1. Security and privacy
  1. Software and application security
    1. Software security engineering
2. Software and its engineering
  1. Software creation and management
    1. Software development process management
      1. Software development methods
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
        Access protection

Recommendations

Security policies enforcement using finite and pushdown edit automata

Edit automata have been introduced by J.Ligatti et al. as a model for security enforcement mechanisms which work at run time. In a distributed interacting system, they play a role of a monitor that runs in parallel with a target program and transforms ...
On the transformation of two-way finite automata to unambiguous finite automata
Abstract
This paper estimates the number of states in an unambiguous finite automaton (UFA) that is sufficient and in the worst case necessary to simulate an n-state two-way deterministic finite automaton (2DFA) and an n-state two-way unambiguous finite ...
On the Transformation of Two-Way Deterministic Finite Automata to Unambiguous Finite Automata
Language and Automata Theory and Applications
Abstract
The paper estimates the number of states in an unambiguous finite automaton (UFA) that is sufficient and in the worst case necessary to simulate an n-state two-way deterministic finite automaton (2DFA). It is proved that a 2DFA with n states can ... $^{}$ ${\sqrt{}}^{}^{}$

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

FOAL '07: Proceedings of the 6th workshop on Foundations of aspect-oriented languages

March 2007

74 pages

ISBN:9781595936714

DOI:10.1145/1233833

Conference Chair:
William Harrison

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 March 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

AOSD07

AOSD07: 6th International Conference on Aspect-Oriented Software Development

March 13, 2007

British Columbia, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 5 of 6 submissions, 83%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
223
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ebnenasir A(2015)Incremental Realization of Safety Requirements: Non-determinism vs. ModularityFundamentals of Software Engineering10.1007/978-3-319-24644-4_11(159-175)Online publication date: 12-Nov-2015
https://doi.org/10.1007/978-3-319-24644-4_11
Gorbovitski MLiu YStoller SRothamel TKiselyov OThompson S(2012)Composing transformations for instrumentation and optimizationProceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation10.1145/2103746.2103759(53-62)Online publication date: 23-Jan-2012
https://dl.acm.org/doi/10.1145/2103746.2103759
Liu YGorbovitski MStoller S(2009)A language and framework for invariant-driven transformationsACM SIGPLAN Notices10.1145/1837852.162161745:2(55-64)Online publication date: 4-Oct-2009
https://dl.acm.org/doi/10.1145/1837852.1621617
Liu YGorbovitski MStoller SSiek JFischer B(2009)A language and framework for invariant-driven transformationsProceedings of the eighth international conference on Generative programming and component engineering10.1145/1621607.1621617(55-64)Online publication date: 4-Oct-2009
https://dl.acm.org/doi/10.1145/1621607.1621617

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents