Skip to main content
Erschienen in: Programming and Computer Software 4/2023

01.08.2023

Scenario of Information Flow Analysis Implementation in PL/SQL Program Units with PLIF Platform

verfasst von: A. A. Timakov

Erschienen in: Programming and Computer Software | Ausgabe 4/2023

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Formal proof of security measure effectiveness and computation security is vitally important for trust in critical information systems. It should be realized that formal security verification must be carried out at each infrastructural level (from the hardware level to the application level) in the process of system design. Currently, computation security analysis on the application level remains the major challenge as it requires complex labeling of computing environment elements. Traditionally, to solve this problem, information flow control (IFC) methods are employed. Unlike access control mechanisms widely used in modern operating systems (OSs) and database management systems (DBMSs), IFC has limited application in software design and mostly comes down to trivial taint tracking. This paper describes an approach to full-fledged implementation of IFC in PL/SQL program units with the use of the PLIF platform. In addition, a general scheme of computation security analysis for enterprise applications that work with relational DBMSs is considered. The key advantage of our approach is the explicit separation of functions between software developers and security analysts.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
By the global variables of the computing environment, we mean attributes of relations.
 
2
The fulfillment of the CompInv property can be achieved in a finite number of iterations, because the policy alphabet is a finite lattice and the transition functions for calculating policies of global variables are monotonically increasing.
 
3
Specifications generated by PLIF describe the state of each user session, including the domain of local variables and parameters (stack), pointers to the current stack frame and to the instruction currently executed in the session, and the domain of return values.
 
Literatur
1.
Zurück zum Zitat Latham, D.C., Department of defense trusted computer system evaluation criteria, 1986. Latham, D.C., Department of defense trusted computer system evaluation criteria, 1986.
2.
Zurück zum Zitat Infrastructure, P.K. and Profile, T.P., Common criteria for information technology security evaluation, 2002. Infrastructure, P.K. and Profile, T.P., Common criteria for information technology security evaluation, 2002.
3.
Zurück zum Zitat Devyanin, P.N. and Leonova, M.A., Use of subtypes and total functions of the formal Event-B method for description and verification of the MROSL DP model, Program. Inzheneriya, 2020, vol. 11, no. 4, pp. 230–241.CrossRef Devyanin, P.N. and Leonova, M.A., Use of subtypes and total functions of the formal Event-B method for description and verification of the MROSL DP model, Program. Inzheneriya, 2020, vol. 11, no. 4, pp. 230–241.CrossRef
4.
Zurück zum Zitat Timakov, A.A., Information flow control in software DB units based on formal verification, Program. Comput. Software, 2022, vol. 48, pp. 265–285.MathSciNetCrossRefMATH Timakov, A.A., Information flow control in software DB units based on formal verification, Program. Comput. Software, 2022, vol. 48, pp. 265–285.MathSciNetCrossRefMATH
5.
Zurück zum Zitat Denning, E.D., A lattice model of secure information flow, Commun. ACM, 1976, no. 5, pp. 236–243. Denning, E.D., A lattice model of secure information flow, Commun. ACM, 1976, no. 5, pp. 236–243.
6.
Zurück zum Zitat Shaitura, S.V. and Pitkevich, P.N., Data backup methods for critical enterprise information systems, Ross. Tekhnol. Zh., 2022, vol. 10, no. 1, pp. 28–34. Shaitura, S.V. and Pitkevich, P.N., Data backup methods for critical enterprise information systems, Ross. Tekhnol. Zh., 2022, vol. 10, no. 1, pp. 28–34.
7.
Zurück zum Zitat Timakov, A., PLIF, 2021. https://github.com/timimin/plif. Timakov, A., PLIF, 2021. https://​github.​com/​timimin/​plif.​
8.
Zurück zum Zitat Konnov, I., Kukovec, J., and Tran, T.-H., TLA+ model checking made symbolic, Proc. ACM Programming Languages, 2019, vol. 3, pp. 1–30. Konnov, I., Kukovec, J., and Tran, T.-H., TLA+ model checking made symbolic, Proc. ACM Programming Languages, 2019, vol. 3, pp. 1–30.
9.
Zurück zum Zitat Broberg, N. and Sands, D., Paralocks: Role-based information flow control and beyond, Conf. Rec. Annu. ACM Symp. Principles of Programming Languages, 2010, pp. 431–444. Broberg, N. and Sands, D., Paralocks: Role-based information flow control and beyond, Conf. Rec. Annu. ACM Symp. Principles of Programming Languages, 2010, pp. 431–444.
10.
Zurück zum Zitat Broberg, N. and Sands, D., Flow locks: Towards a core calculus for dynamic flow policies, Lect. Notes Comput. Sci., 2006, pp. 180–196. Broberg, N. and Sands, D., Flow locks: Towards a core calculus for dynamic flow policies, Lect. Notes Comput. Sci., 2006, pp. 180–196.
11.
Zurück zum Zitat Broberg, N., Practical flexible programming with information flow control, Thesis for the Degree of Doctor of Engineering, 2011. Broberg, N., Practical flexible programming with information flow control, Thesis for the Degree of Doctor of Engineering, 2011.
12.
Zurück zum Zitat Hedin, D. and Sabelfeld, A., A perspective on information-flow control, Software Saf. Secur., 2012, pp. 319–347. Hedin, D. and Sabelfeld, A., A perspective on information-flow control, Software Saf. Secur., 2012, pp. 319–347.
13.
Zurück zum Zitat Methni, A., Lemerre, M., Hedia, B.B., Barkaoui, K., and Haddad, S., An approach for verifying concurrent C programs, Proc. 8th Jr. Res. Workshop Real-Time Computing, 2014, pp. 33–36. Methni, A., Lemerre, M., Hedia, B.B., Barkaoui, K., and Haddad, S., An approach for verifying concurrent C programs, Proc. 8th Jr. Res. Workshop Real-Time Computing, 2014, pp. 33–36.
14.
Zurück zum Zitat Fernandes, A., tlaplus-graph-explorer, 2021. https://github.com/afonsonf/tlaplusgraph-explorer. Fernandes, A., tlaplus-graph-explorer, 2021. https://​github.​com/​afonsonf/​tlaplusgraph-explorer.​
15.
Zurück zum Zitat Kozyri, E. et al., Expressing information flow properties, Found. Trends Privacy Secur., 2022, vol. 3, no. 1, pp. 1–102.CrossRef Kozyri, E. et al., Expressing information flow properties, Found. Trends Privacy Secur., 2022, vol. 3, no. 1, pp. 1–102.CrossRef
16.
Zurück zum Zitat Kristensen, E., CodeQL, 2022. https://github.com/github/codeql. Kristensen, E., CodeQL, 2022. https://github.com/github/codeql.
17.
Zurück zum Zitat Delfit, V.B., Broberg, N., and Sands, D., A Datalog semantics for Paralocks, Lect. Notes Comput. Sci., 2013, pp. 305–320. Delfit, V.B., Broberg, N., and Sands, D., A Datalog semantics for Paralocks, Lect. Notes Comput. Sci., 2013, pp. 305–320.
18.
Zurück zum Zitat Harrison, M.A., Ruzzo, W.L., and Ullman, J.D., Protection in operating systems, Commun. ACM, 1976, vol. 19, no. 8, pp. 461–471.CrossRefMATH Harrison, M.A., Ruzzo, W.L., and Ullman, J.D., Protection in operating systems, Commun. ACM, 1976, vol. 19, no. 8, pp. 461–471.CrossRefMATH
Metadaten
Titel
Scenario of Information Flow Analysis Implementation in PL/SQL Program Units with PLIF Platform
verfasst von
A. A. Timakov
Publikationsdatum
01.08.2023
Verlag
Pleiades Publishing
Erschienen in
Programming and Computer Software / Ausgabe 4/2023
Print ISSN: 0361-7688
Elektronische ISSN: 1608-3261
DOI
https://doi.org/10.1134/S0361768823040114

Weitere Artikel der Ausgabe 4/2023

Programming and Computer Software 4/2023 Zur Ausgabe

Premium Partner