Communication security formalization analysis and verification system in process based on micro kernel prototyping

Abstract

The invention discloses a communication security formalization analysis and verification system in process based on a micro kernel prototyping. The communication security formal analysis and verification system comprises a prototype preprocessed module. The prototype preprocessed module comprises a system entrance of the formalization analysis and verification system, and an embedded operating system micro kernel prototype is as input. A pending verified IPC module extracted from the micro kernel module classified processes to generate a collection IPC with related function as inputting pending verified data of each module. An IPC security properties of a particular attribute in a finite state is verified through a denumerable state specific attribute authentication module. The denumerable state specific attribute authentication module is capable of modeling and analyzing the pending verified IPC fault behavior pointedly. An Infinite state and the generalized attribute verification module are used for verifying IPC security properties of infinite and non-specific attributes, verifying the external nature of IPC abstracted from a standardized data structure, and deeply abstracting and further generating different models and refine validation based on abstract properties and each interest point.

Description

technical field [0001] The invention belongs to the field of embedded systems, relates to model detection and theorem proving technologies, in particular to a formalized analysis and verification system for inter-process communication security based on an embedded operating system microkernel prototype. Background technique [0002] On the one hand, with the rapid development of computer technology, a type of embedded micro-kernel operating system with the characteristics of simplified kernel, strong specialization, and easy maintenance has gradually become popular, and has been widely used in various aspects such as medical care, military industry, and people's livelihood. . On the other hand, due to the design concept of implementing most of the functions in the kernel of the traditional macro-kernel operating system, as time goes by, it is inevitable that the amount of code will be extremely large, the size of the kernel will expand rapidly, the dependencies between modul...

AI Technical Summary

Problems solved by technology

Among them, the typical solutions used in simulation and traditional testing are to design logic test cases with different coverage standards, and to observe whether the result signal is wrong through input signals. This kind of test solution is difficult to guarantee the comprehensiveness and accuracy of verification in today's increasingly complex operating system. sex

Images