Use of the PVS formal logic system in the method of formal proof of security in the construction of information security systems
DOI:
https://doi.org/10.15587/2706-5448.2021.229539Keywords:
information and telecommunication system, information security system, security policy, method of formal proof of security, specification languageAbstract
The object of research is the information and telecommunication system (ITS) and ensuring the protection of information stored, processed and circulating in it. One of the most problematic areas in the creation of secure ITS is the logical inconsistency and incompleteness of the information security policy. That is, a set of laws, rules, restrictions, recommendations, etc., which regulate the procedure for processing information and are aimed at protecting information from a certain set of threats. The reason for such problems is usually the absence of pre-design modeling of the information security system as a component of the information and telecommunications system, which in the end causes the latter to be vulnerable.
An important prerequisite for the creation of a secure ITS is the construction of a subject-object model of the system, which makes it possible to determine the connections between objects, their features, to model information flows and types of access to information and infrastructure resources. According to the existing clear, complete and consistent subject-object model of the ITS, it becomes possible to apply mathematical methods to modeling the processes of its functioning, including for solving the problem of formal proof of security.
The paper considers the main idea of the method of formal proof of security, which can be used when building information security systems or assessing the security of the created information and telecommunications system. It is shown that for its implementation it is possible to use the methodology of automatic theorem proving. One of the ways to solve this problem, which is proposed in the work, is the use of the PVS (Prototype Verification System) formal logic system, which is widely used for writing specifications and constructing proofs. The main components of this system are considered, as well as the possibilities of its use for automatic proof of statements about the impossibility of unauthorized access under the conditions of a certain security policy. An example of the use of the PVS system for the formal proof of the security of the system in the framework of the Bella-LaPadula security policy is given.
References
- Antoniuk, A. A., Zhora, V. V. (2005). Obobshchenye modely uhroz v ynformatsyonno-telekommunykatsyonnoi systeme. Pravove, normatyvne ta metrolohichne zabezpechennia systemy zakhystu informatsii v Ukraini, 11, 50–54.
- Glushkov, V. M. (1980). Sistema avtomatizatsii dokazatelstv. Avtomatizatsiia obrabotki matematicheskikh tekstov. Kyiv: IK AN USSR, 3–30.
- Bishop, M. (2018). Computer Security Art and Science. Addison Wesley Professional, 2865.
- Owre, S., Shankar, N., Rushby, J. M., Stringer-Calvert, D. W. J. (2020). PVS System Guide Version 7.1. SRI International. Available at: https://pvs.csl.sri.com/doc/pvs-system-guide.pdf
- Owre, S., Shankar, N. Rushby, J. M., Stringer-Calvert, D. W. J. (2020). PVS Language Reference Version 7.1. SRI International. Available at: https://pvs.csl.sri.com/doc/pvs-language-reference.pdf
- Owre, S., Shankar, N., Rushby, J. M., Stringer-Calvert, D. W. J. (2020). PVS Prover Guide Version 7.1. SRI International. Available at: https://pvs.csl.sri.com/doc/pvs-prover-guide.pdf
- Antoniuk, A. O., Zhora, V. V. (2007). Vikoristannia dokazovogo metodu dlia proektuvannia ta otsіnki rіvnia zakhischenostі іnformatsіino-telekomunіkatsіinoї sistemi. Problemi programuvannia, 3, 88–96.
- Muñoz, C. A., Demasi, R. A.; Meyer, B., Nordio, M. (Eds.) (2012). Advanced Theorem Proving Techniques in PVS and Applications. Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 7682. doi: http://doi.org/10.1007/978-3-642-35746-6_4
- McGuinness, D. L.; Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., Patel-Schneider, P. F. (Eds.) (2010). The Description Logic Handbook. Theory, Implementation and Applications. Cambridge: University Press, 624. doi: http://doi.org/10.1017/cbo9780511711787
- Turhan, A. Y.; Rudolph, S., Gottlob, G., Horrocks, I., van Harmelen, F. (Eds.) (2013). Introductions to Description Logics – A Guided Tour. Reasoning Web. Semantic Technologies for Intelligent Data Access. Reasoning Web 2013. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 8067. doi: http://doi.org/10.1007/978-3-642-39784-4_3
- Bell, D. E., La Padula, L. J. (1976). Secure Computer Systems: Mathematical foundations and model. Report ESD-TR-73-278. Mitre Corp. Bedford. Available at: http://www-personal.umich.edu/~cja/LPS12b/refs/belllapadula1.pdf
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2021 Віктор Володимирович Жора, Олександр Борисович Синецький
This work is licensed under a Creative Commons Attribution 4.0 International License.
The consolidation and conditions for the transfer of copyright (identification of authorship) is carried out in the License Agreement. In particular, the authors reserve the right to the authorship of their manuscript and transfer the first publication of this work to the journal under the terms of the Creative Commons CC BY license. At the same time, they have the right to conclude on their own additional agreements concerning the non-exclusive distribution of the work in the form in which it was published by this journal, but provided that the link to the first publication of the article in this journal is preserved.
