A semantic-based transaction processing model for multilevel transactions 1

Abstract

Multilevel transactions have been proposed for multilevel secure databases; in contrast to most proposals, such transactions allow users to read and write across multiple security levels. The security requirement that no high level operation influence a low level operation often conflicts with the atomicity requirement of the standard transaction processing model. In particular, others have shown that no concurrency control algorithm based on the standard transaction processing model can guarantee both atomicity and security. This conflict motivates us to propose an alternative semantic-based transaction processing model for multilevel transactions. Our model uses the semantics of the application to analyze an application and reason about its behavior. Our notion of correctness is based on semantic correctness instead of serializability as in the standard transaction processing model. Semantic correctness ensures that database consistency is maintained, transactions output consistent data, and all partially executed transactions complete. We show how an example application can be analyzed to assure semantic correctness and how this analysis can be automated. We also propose a simple timestamp-based multiversion concurrency control algorithm for transaction processing on a kernelized architecture. The advantages of our model over the standard transaction processing model are that atomicity can be assessed, and for some applications ensured via off line analysis, more concurrency is achieved, lesser synchronization between security levels is required, and a larger class of multilevel transactions can be processed.

Get full access to this article

View all access options for this article.

References

Agrawal,

El Abbadi and

A.K.

Singh, Consistency and orderability: Semantics-based correctness criteria for databases, ACM Transactions on Database Systems 18(3) (September 1993), 460–486.

J.M.

Atlee and

J.D.

Gannon, State-based model checking of event driven systems requirements, IEEE Transactions on Software Engineering 19(1) (January 1993), 13–23.

Ammann,

Jajodia and

Ray, Using formal methods to reason about semantics-based decomposition of transactions, in: Proceedings of the International Conference on Very Large Databases, Zurich, Switzerland, September 1995, pp. 218–227.

Ammann,

Jajodia and

Ray, Ensuring atomicity of multilevel transactions, in: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, May 1996, pp. 74–84.

Ammann,

Jajodia and

Ray, Applying formal methods to semantic-based decomposition of transactions, ACM Transactions on Database Systems 22(2) (June 1997), 215–254.

P.A.

Bernstein,

Hadzilacos and

Goodman, Concurrency Control and Recovery in Database Systems, Addison-Wesley, Reading, MA, 1987.

B.T.

Blaustein,

Jajodia,

C.D.

McCollum and

Notargiacomo, A model of atomicity for multilevel transactions, in: Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, May 1993, pp. 120–134.

D.E.

Bell and

L.J.

LaPadula, Secure computer system: Unified exposition and multics interpretation, Technical Report MTR-2997, The MITRE Corporation, Bedford, MA, July 1975.

Bernstein and

Lewis, High performance transaction systems using transaction semantics, Distributed and Parallel Databases 4(1) (1996), 25–47.

10.

E.M.

Clarke,

Grumberg and

Long, Verification tools for finite-state concurrent systems, in: A Decade of Concurrency – Reflections and Perspectives, Lecture Notes in Computer Science, Vol. 803, Springer Verlag, Berlin, 1994.

11.

Costich and

Jajodia, Maintaining multilevel transaction atomicity in multilevel secure database systems with kernelized architecture, in: Database Security VI: Status and Prospects,

B.M.

Thuraisingham and

C.E.

Landwehr, eds, North-Holland, Amsterdam, 1993, pp. 249–265.

12.

Costich and

McDermott, A multilevel transaction problem for multilevel secure database system and its solution for the replicated architecture, in: Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, May 1992, pp. 192–203.

13.

A.A.

Farrag and

M.T.

Özsu, Using semantic knowledge of transactions to increase concurrency, ACM Transactions on Database Systems 14(4) (December 1989), 503–525.

14.

Garcia-Molina, Using semantic knowledge for transaction processing in a distributed database, ACM Transactions on Database Systems 8(2) (June 1983), 186–213.

15.

Garcia-Molina and

Salem, Sagas, in: Proceedings of ACM-SIGMOD International Conference on Management of Data, San Francisco, CA, 1987, pp. 249–259.

16.

Gray and

Reuter, Transaction Processing: Concepts and Techniques, Morgan Kaufmann Publishers, San Francisco, CA, 1993.

17.

Jackson, Niptick: A checkable specification language, in: Proceedings of the Workshop on Formal Methods in Software Practice, San Diego, CA, January 1996.

18.

H.F.

Korth and

Speegle, Formal aspects of concurrency control in long-duration transaction systems using the NT/PV model, ACM Transactions on Database Systems 19(3) (September 1994), 492–535.

19.

K.L.

McMillan, Symbolic model checking: an approach to the state explosion problem, PhD thesis, Carnegie Mellon University, Pittsburgh, PA, 1992.

20.

Owicki and

Gries, Verifying properties of parallel programs: An axiomatic approach, Communications of the ACM 19(5) (May 1976), 279–285.

21.

Owre,

J.M.

Rushby and

Shankar, PVS: A prototype verification system, in: Proceedings of the International Conference on Automated Deduction,

Kapur, ed., Saratoga, NY, June 1992, pp. 748–752.

22.

Rastogi,

H.F.

Korth and

Silberchatz, Exploiting transaction semantics in multidatabase systems, in: Proceedings of the International Conference on Distributed Computing Systems, Vancouver, Canada, June 1995, pp. 101–109.

23.

R.S.

Sandhu, Lattice-based access control models, IEEE Computer 26(11) (November 1993), 9–19.

24.

K.P.

Smith,

B.T.

Blaustein,

Jajodia and

Notargiacomo, Correctness criteria for multilevel secure transactions, IEEE Transactions on Knowledge and Data Engineering 8(1) (February 1996), 32–45.

25.

J.M.

Spivey, The Z Notation: A Reference Manual, 2nd edn, Prentice-Hall, Englewood Cliffs, NJ, 1992.

26.

J.M.

Wing and

Vazari-Farahani, A case study in model checking software systems, Technical Report CMU-CS-96-124, Carnegie Mellon University, Pittsburgh, PA, April 1996. To appear in Science of Computer Programming.