CN1752945A - Method for Generating Test Cases of Security Database Management System - Google Patents

Abstract

The present invention proposes for the first time a systematic and operable method for generating test cases of a security database management system, which includes the following steps: 1) generating a test protocol, based on the formalized protocol describing the system operation function and the security axiom requirements of the operation Generate test specifications for each operation in the system; 2) Generate test templates, perform equivalent transformations on test specifications according to certain rewriting rules, and express them in the form of disjunctive normal form, so that the test specifications of operations can be equivalently represented as a set Test template; 3) type division, perform heuristic equivalent transformation on the types existing in the system, and further subdivide the test space represented by each test template; 4) generate test vectors, test each test sub-domain, and instance to generate corresponding test vectors. This method is based on the security model of the system under test, and the test results are complete, scientific, repeatable and internally consistent.

Description

Method for Generating Test Cases of Security Database Management System

technical field

The invention belongs to the field of testing and evaluation of computer software, and mainly relates to the testing and evaluation of a secure database management system (SecureDataBase Management System, referred to as SDBMS), more precisely, the generation of test cases for a high-security database management system based on the SDBMS security strategy model method.

Background technique

Software testing is an effective means to check the consistency between software implementation and its functional specifications, and to ensure software quality. In the process of evaluating information security products based on security evaluation standards, it is an indispensable and important link in the evaluation that the evaluator conducts comprehensive and systematic third-party testing of the security functions of the security system. However, due to many reasons, the independent security function test does not occupy an important position in the evaluation of our country's security database management system. The key problem is how to implement the organization and design of test cases. At present, there is a lack of a systematic method to quickly generate test case sets for specific information security products/systems (including SDBMS).

Due to restrictions such as software copyright rights, third-party independent testing mostly uses protocol-based testing. The system specification is derived from the system requirements, which completely defines the behavior of the system. Protocol-based testing can determine the impact relationship between input and output, effectively ensuring the comprehensiveness of software functional testing. Formal specification is a more precise expression form of system specification, which can better eliminate the ambiguity in system requirements. At the same time, the formal specification provides a canonical form of expression, thus facilitating its automatic processing. Automatically generating test cases according to the formal safety specification will greatly reduce the testing workload. A current practice is to divide the test space according to certain rewriting rules through functional specification modeling, and automatically generate test cases.

However, the direct application of the above methods in the test and evaluation of SDBMS systems will lead to some special problems: the above-mentioned formal functional specification rewriting rules (or heuristics) are purely related to syntax and have nothing to do with semantics, so the generated test cases lack Targeted, it is difficult to find problems in specific systems. In addition, the input variable space of each operation in the SDBMS system is limited, but the internal state space of the system is very large, almost infinite. The above method is only suitable for smaller-scale systems, and cannot be directly applied to the evaluation of SDBMS systems.

More importantly, for most information security products including SDBMS, the system specification cannot truly reflect the behavior of the real system. Because the operations in the system must meet the security policy requirements in addition to completing their intended functions. A security policy describes the objects to be protected by an information security product (or system) and all protective measures taken. There are security policies at different levels of abstraction, such as the system's security goals, and the system's security policy model. There is a formal security policy model in the high security level SDBMS.

Another approach is to build precise formal safety function models by modeling informal safety goals. The problem with this approach is that because of the manual modeling process of the evaluators, the model and the final test results are heavily dependent on the correct understanding of the informal security goals provided by the developers. In addition, the granularity of the security policy in the security target is relatively coarse, requiring the evaluators to correspond the subjects and objects in the security policy with the actual system objects one by one.

Contents of the invention

In view of the above problems, the object of the present invention is to provide a test case generation method based on the SDBMS security policy model. Basic prerequisites for this test method include:

1. An SDBMS security policy model:

The correctness of the model is proved by formal tools. A typical formalized SDBMS security policy model has the following elements: (1) state set (STATES), which describes the legal state of the system; (2) security axiom set (ANXIOMS), security axioms are a set of properties defined in the model, a certain A system state S is safe if and only if it satisfies these properties; (3) operation set (OPS), the transition of the system state is realized by the system operation, and each operation is controlled, only when it produces a safe state Only when it is allowed to execute, that is, it satisfies all the properties in the model; (4) Security theorem set (THEOREMS), which can prove some security properties satisfied by the abstract security model.

2. A set of SDBMS products to be tested:

The product is implemented based on the aforementioned SDBMS security policy model, and the two have been confirmed to be consistent by the developer.

3. The high-level specification of the SDBMS to be tested, and the specific interface definition document of the product.

The test case generation method based on the SDBMS security model provided by the present invention is based on the following ideas: the formalized security policy model is the basis for generating SDBMS security function test cases, and the basic idea of the test case generation method is to determine the test state space, and The test space (including the input state space and the intermediate state space) is divided. Because according to the unified hypothesis (unified hypothesis) idea in test theory, all inputs and states in each partition should behave the same. Therefore, one or several examples are selected for testing in each division.

This method includes two types of test space division strategies: one is sub-domain division. Divide the test space into test subdomains. Each subdomain is described by an abstract test template; the other is type division. The type value of the variable is divided, and the test template is instantiated into a specific test case.

Specifically, the method includes the following four steps:

Step 1: Generate test specification. Because the premise of generating test cases is an accurate and complete formal test specification, so in the first step, the test specification must be generated according to the formal specification describing the operation function and the safety axiom requirements of the operation.

Step 2: Generate a test template. Step 2 divides the test space defined by the test protocol into sub-domains by rewriting the test protocol. The subdomains are disjoint, and each test subdomain corresponds to a test template.

Step 3: Type division. Step 3 provides a division method different from Step 2—type division. Type partitioning further divides the test space on the basis of test sub-domains.

Step 4: Generate test vectors. Combining the above two division methods, in step 4, each test sub-domain is checked and instantiated to generate corresponding test vectors to form a complete test case.

The following uses the SDBMS model described in Z language as an example to illustrate the contents of the above four steps. The idea of this step can be naturally applied to SDBMS models described in other formal languages. constitute any restrictions.

Step 1: Generate a test specification

The test specification of an operation in the SDBMS system fully and accurately reflects the behavior of the operation. Specifically, the test specification for a member operation op in the SDBMS security model operation set consists of the following three parts:

(1) The basic definition of the operation op in the SDBMS model:

The declaration part of the basic definition of the operation op in the SDBMS model includes the input variable set ins of the operation, the output variable set outs, and the intermediate state variable set Δstate before and after the operation. The predicate part in the basic definition of operation can be divided into two categories according to semantics: one is the precondition constraint of operation op, marked as P; the other is the change of system state caused by the operation, marked as Q. Their meanings are: if and only if the precondition constraint P is satisfied, the operation op is executed, and the state change of the system will satisfy Q after the correct execution. For example, the basic definition of the operation op expressed in Z language shcema form is:

The formal definition of the operation must meet the requirements of consistency and completeness. The consistency requirement means that the precondition constraints of the operation are satisfyable; the completeness requirement means that there is no remaining definition domain, and its operation result is not defined. If the description of when the operation constraint is not satisfied is supplemented on the basic operation definition, add the operations non_op, Success, and Fail as defined above. Then constitute an operation of the following form:

Because pre op_full=true, the operation op_full is a consistent and complete operation.

(2) Operation-related security axioms (sets) in the SDBMS model:

Most operations in the SDBMS security policy model must satisfy certain security axioms (sets). For example, a certain SDBMS security policy model requires that the insert and delete operations on data objects should satisfy the static constraints and dynamic constraints in the role-based access control model. The set of security axioms that an operation op must satisfy is expressed as a function axioms(op). Security axioms are usually expressed as predicate constraints, which are directly related to the security policies defined by the system and reflect the security properties required by the system. This method distinguishes the security property constraints from the semantic constraints of the operation itself, making the structure of the SDBMS security policy model clearer.

The basic definition and supplementary definition of the operation op after adding the security axiom constraints are adjusted to op′ and non_op′ respectively:

Similarly, the complete operation after adding the security axiom constraint is expressed as:

(3) Fixed constraints existing in system-related intermediate state variables:

操作op的基础定义及补充定义可进一步调整为op″与non_op″：In fact, in addition to being constrained by the precondition P, the operation op must also satisfy some constraints not directly related to the operation. These constraints limit the relationship between the intermediate variables of the system, and only a state that satisfies these fixed constraints can be a legal system state. These constraints are thus implied by the state before the operation op occurred. If these fixed constraints are represented by the symbol TCB, the operation specification should actually be:

The basic definition and supplementary definition of the operation op can be further adjusted to op" and non_op":

The complete operation is expressed as:

TCB在实际系统中是不可达的。若SDBMS安全模型中存在类似的初始化定理并予以证明，则考虑到操作的完整性要求，操作op的完整定义仍然等价于op_full′。Because any state of the system must satisfy the TCB constraint, the state

TCB is not reachable in practical systems. If a similar initialization theorem exists in the SDBMS security model and is proved, then considering the integrity requirements of the operation, the complete definition of the operation op is still equivalent to op_full'.

To sum up, for the operation op in the SDBMS security policy model, according to whether there is a proven initialization theorem, the test specification op_test composed of the above three parts can be finally expressed as the following form:

$\mathrm{op}\_\mathrm{test}\widehat{=}\mathrm{op}\_{\mathrm{full}}^{\′\′}$ or $\mathrm{op}\_\mathrm{test}\widehat{=}\mathrm{op}\_{\mathrm{full}}^{\′}$

Step 2: Generate a test template

The test specification of an operation accurately describes the behavioral characteristics of the operation, and also limits the test space of the operation. But before generating test cases for this operation, the test space must be divided into a series of disjoint test sub-domain spaces. According to specific rewriting rules, we perform equivalent transformation on the predicate constraint part in the test specification, and simplify it into the form of disjunctive normal form (DNF), so that the test specification op_test of the operation op is equivalently expressed as a set of test templates.

The rewriting rules used by the equivalent transformation cannot be listed one by one, and the main rules include:

(1) There are quantifier elimination rules (single-point rules):

(2) full quantifier elimination rule:

(3) Distributive rules:

其中第i个测试模版op_templatei为单纯合取式，表示为 按照所代表的语义分为三类：p_i表示第i个测试模版的约束，它是一个谓词或多个谓词的合取式，

q_i表示操作执行后第f个测试模版的状态变化，

r_i为第i个测试模版的输出结果集，

The rewritten test specification is expressed as a disjunction of n test templates:

Among them, the i-th test template op_templatei is a simple conjunction, expressed as According to the represented semantics, it is divided into three categories: p _i represents the constraint of the i-th test template, which is a predicate or a conjunction of multiple predicates,

q _i represents the state change of the fth test template after the operation is executed,

r _i is the output result set of the i-th test template,

The generated test template set {op_template _i }, (1≤i≤n) satisfies the following two properties:

①i, j: 1..n·i≠j|pi∧p _j = false.

Property ① It shows that there is no intersection between the constraints of each test template in the test template set, and the generated test template divides the test space into a group of disjoint test sub-domains, and each test template represents a test sub-domain. Property ② shows that the set of test templates is complete, covering all the test space of the operation under test. That is to say, the precondition of this operation is eternal truth, pre op_test=true.

It should be pointed out that the application order and number of the above rules may be different, and the disjunctive normal form (DNF) obtained after equivalent transformation of a given test specification is not unique. And the equivalence transformation may introduce some indirect input variables to the operation.

Step 3: Type division

In most cases, the number of test templates generated in step 2 is very limited, and step 3 performs heuristic equivalent transformation on each test template by type division to further subdivide the test space. First, clarify the concept of division and type.

Let A be a non-empty type, if there exists a subset family π(πP(A)) of A that satisfies the following conditions:

(1)

(2) Any two elements in π do not intersect

(3) The union of all elements in π is equal to A

Then π is called a partition of type A, and the elements in π are called partition blocks. The union of all elements in π is called a π-partitioned representation of type A.

The division on the SDBMS security policy model comes down to the following four situations.

Case 1: Preset value division:

If there is a series of special preset values s ₁ , s ₂ , ... s _n in type T, then the preset value division of type T divides the type into π: π={{s ₁ ), {s ₂ }, ..., {s _n }, {t: T|t≠s ₁ ∧t≠s ₂ ∧…∧t≠s _n }}, according to the division π, the type T can be expressed as T={s ₁ }∨{s ₂ } ∨…{s _n }∨{t: T|t≠s ₁ ∧t≠s ₂ ∧…∧t≠s _n }.

Special values in a type are system defaults, have special meaning compared to other values in that type, and should be tested individually. And because there is no intersection of these values, each special value in the type is a subset of the type space partition, which satisfies the definition requirements of the partition.

Case 2: Function value division:

If there is a function f from type T to type V: T→V, and type V is a finite set, ran(f)={v ₁ , v ₂ ,...v _n ). Then the function value of type T is divided into π as: π={{t: T|f(t)=v ₁ }, {t: T|f(t)=v ₂ }, ..., {t: T |f(t)=v _n }}. If the type V is an infinite set, but there is an important partition π ₀ ={{s ₁ },{s ₂ },...,{s _n }}, then the type T has an extended function value partition: π′={{ t: T|f(t)∈s ₁ ), {t: T|f(t)∈s ₂ }, ..., {t: T|f(t)∈s _n }}.

There may be some functions on each type in the SDBMS model. A group of variables with the same function value represents a class of values with the same property, and different function values may correspond to different behaviors in the model, so it can be based on different Function evaluation divides the variables in the type into different subsets for testing.

Case 3: Set partitioning:

If there are multiple data sets on type T, they are expressed as ts ₁ , ts ₂ , . . . ts _n respectively, that is, for any 1≤i≤n, ts _i =ρ(T). Then the set division of type T can be expressed recursively as follows:

1)

2) For any 1<i≤n:

3) The type T can finally be expressed as: T=T_test(n).

Similar to functions, each data set in the SDBMS model represents a class of values with the same properties, and the combination of these properties is considered to the greatest extent in the division of sets. Since most data sets form part of the system state, set partitioning is usually only applied to input variables.

Case 4: Data partitioning:

This situation involves some common data types, such as integer types, natural number types, Boolean types, and so on. The special values of these data types are inherently special values related to the type, for example, the data that exists on the Boolean type is divided into {true, false}. Data division is very similar to default value division in form, the main difference is that data division is applied to types whose members are known, while default value division is applied to types whose number of members and content are uncertain.

Theoretically, if there is a function on a certain type, function division should be used; if there is a set, set division should be used; and so on. If the above-mentioned multiple divisions exist at the same time for the same type, their comprehensive division needs to be calculated. The calculation of composite partitions depends on the relationship between these partitions. If any partition block in partition A intersects with any partition block in partition B, it is said that the two partitions are in an orthogonal class relationship; The union of the intersection between the division blocks of A and B. If any partition block in partition A belongs to a certain partition block in partition B, it is said that there is an overlapping class relationship between the two. The composite partition of the two partitions of overlapping class relations is equivalent to the partition of B. There is another class between the orthogonal class and the overlapping class, that is, some partition blocks intersect and some partition blocks overlap. The comprehensive division calculation of this type of relationship is also a combination of the two.

It is conceivable that if there are many orthogonal class divisions on a certain type, and each division contains a large number of division blocks, it is very likely that the combination explosion of the test space division will occur. Therefore, some trade-offs need to be made for the application of partitioning principles. Here we give two orthogonal class division and trade-off principles:

(1) Prioritize m-select-n principle (m≥n). If there are m orthogonal partitions π _i (1≤i≤m) on the type T, arrange them in non-decreasing order of importance, and calculate the comprehensive partition of the first n partitions based on the m-select-n principle.

The type T can be divided into T_test _i (1≤i≤m) according to different divisions, and its length is | _πi |. After sorting in non-decreasing order of importance, the first n are divided into π _i (1≤i≤n). The comprehensive division P of the priority m-select-n principle on type T is:

The maximum length of the comprehensive division is: $\mathrm{num}=\underset{1\&le;i\&le;\mathrm{no}}{\mathrm{\&Pi;}}\left(\right|{\mathrm{\&pi;}}_i\left|\right),$ Its content is:

(partion_i∈π_i)

(partition _i ∈ π _i )

(2) Orthogonal m-select-n principle (m≥n). If there are m orthogonal partitions π _i (1≤i≤m) on the type T, the comprehensive partition calculated by the orthogonal m-select-n principle includes the partition blocks of the comprehensive partition of any n partitions.

The type T can be divided into T_test _i (1≤i≤m) according to different divisions, and its length is | _πi |. After being arranged in non-increasing order according to the division length, the first n divisions are recorded as πi (1≤i≤n). Let P denote a synthetic partition of the orthogonal m-select-n principle on type T. P′ represents the comprehensive partition of any n partitions on type T, any partition block p′ _i (p′ _i ∈ P′) in P′, and there is at least one partition block p _i (p _i ∈ P′) in the comprehensive partition P P), satisfying: p _j p′ _i .

The comprehensive partition of the m-choose-n-choose principle for orthogonal partitions on type T is expressed as a disjunctive normal form. The length of the composite division is $\mathrm{num}=\underset{1\&le;i\&le;\mathrm{no}}{\mathrm{\&Pi;}}\left(\right|{\mathrm{\&pi;}}_i\left|\right).$ Its content is:

(partioni∈π_i)

( _{partioni∈πi} )

The calculated comprehensive partition can be directly applied to the partition of the input variables, and can also be indirectly applied to the partition of the internal state space. Because in the final analysis, the internal state is composed of a set of internal variables and their corresponding values.

Step 4: Generate test vectors

In fact, the test space division of the tested operation in the SDBMS model is a combination of the sub-domain division described in step two and the type division described in step three. A complete test vector is the basis for evaluating the SDBMS product to be tested. Specifically, the test vector is the sum of a set of vectors, that is, a quadruple composed of input vector, current state vector, output vector, and state change vector: (IN, pre_STATE, OUT, post_STATE).

The input vector is composed of the input variable set of the operation op and the value of each variable. The value of the input variable depends on the specific test template and type division block, which is the instantiation of the test space division. In addition to the input vector, the execution result of the operation op also depends on the value of the internal state variables of the system during the test. Only when the system state is known can the values of the output vector and state change vector generated by an input vector be determined. For a certain internal state, the relationship between a certain type of division block and the test template may be three types: the division block completely satisfies the test template, that is, any member of the division block can be used as the input of the division instantiation; the division block is not at all Satisfy the test template, that is, none of the members in the division block can satisfy the test template; or the division block partially satisfies the test template. That is, some members in the division block can satisfy the test template, and some cannot. At this time, whether the result satisfies the test template depends on the specific input.

Although all internal state variables can be classified into single-type collections, compound-type collections, and type functions, they can also be divided by type division methods, but there are two problems: one is that the number of internal state variables Too large, this division will lead to state explosion. The second is the controllability of the state, not any legal state is reachable. Even for reachable states, computing the path is an NP problem. Therefore, we select some special known states as test preset states, for example, including the initial state, and a set of states related to indirect input types (must be the post-state of a tested operation). Specific state generation, selection, and traversal methods have been well documented in prior art documents, and those skilled in the art can understand them, so they will not be explained in detail in this specification.

若给定某输入向量IN＝(INs，VALs)，与系统状态pre_STATE，可以计算出逻辑变量(p_k∧pre_STATE)[VALs/INs]的值，若其为真，则该测试用例的预期输出结果为r_k，状态变化为q_k；生成的测试向量为：(IN，pre_STATE，r_k，q_k)。否则不生成测试用例。因为pre op_test＝true，所以对于任何一个状态与输入向量，不论是操作成功或是失败的，必然有一个测试模板使该逻辑变量为真，从而生成相应的测试向量。For test template

Given a certain input vector IN=(INs, VALs) and the system state pre_STATE, the value of the logic variable (p _k ∧ pre_STATE)[VALs/INs] can be calculated, and if it is true, the expected output of the test case The result is r _k , the state change is q _k ; the generated test vector is: (IN, pre_STATE, r _k , q _k ). Otherwise no test cases are generated. Because pre op_test=true, for any state and input vector, whether the operation succeeds or fails, there must be a test template to make the logic variable true, so as to generate the corresponding test vector.

The technical effect of the present invention is that the present invention proposes a systematic and operable method for generating test cases of a security database management system for the first time, which is helpful for scientific, comprehensive and accurate testing of the security functions of such systems . This method is based on the security model of the system under test, and the test results are complete, scientific, repeatable and internally consistent. Compared with the current manual random evaluation method, it can better find the defects of system implementation and greatly improve the test quality. This method combined with formal auxiliary tools can reduce duplication of labor in the testing process, reduce the cost of generating a large number of test cases, and is conducive to the realization of test automation.

Detailed ways

Taking the LOIS security database management system developed by the State Key Laboratory of Information Security, Institute of Software, Chinese Academy of Sciences as an example, the test case generation method for the security database management system provided by the present invention will be described in detail below.

There are two modes of autonomous authorization related operations in the SDBMS model of the system: one is to authorize users directly, and the other is to authorize roles first, and then activate roles by users. The direct authorization operation GrantPermToUser is an administrative operation that requires the existence of an authorized user who has not been granted this permission. It depends on multiple operations, such as creating a user, creating a security label, creating a data object, connecting, etc. Before performing a test for this operation, you should ensure that you have performed a test for the above operation. And any type of users in the system cannot authorize system administrators, security administrators and audit administrators. This operation changes the access control matrix in the system state, which is described in detail as follows:

The operating statute after supplementing completeness is:

The operation GrantPermToUser should satisfy the axiom GrantPermToUser_axiom, that is, the grantor has been granted the permission and is allowed to propagate the permission: or the grantor is the owner of the object privilege. All object privileges are categorized as follows:

dbOwnerPrivs=={ConnectDatabase, CreateDomain, CreateTable, CreateView}

dmOwnerPrivs=={CreateonDomain, DroponDomain, UseDomain, DropDomain}

tbOwnerPrivs=={CreateRule, DropRule, SelectTable, Insert, Delete, DropTable}

viOwnerPrivs=={SelectView, DropView}

The formal description of the axiom GrantPermToUser_axiom is:

Transition·GrantPermToUser

cur-trans-class(T)=osi-class(o?)

∧ $(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}(T,o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix}))$

∨(owner(database-osi(session-database(trans-session(T))))=trans-user(T)

∧p? ∈dbOwnerPrivs)

After step 1, the complete expression of the test specification test_GrantPermToUser that operates GrantPermToUser is:

$\mathrm{<span\; class="notranslate">\; test</span>}<span\; class="notranslate">\; \_</span>\mathrm{<span\; class="notranslate">\; GrantPermToUser</span>}\stackrel{<span\; class="notranslate">\; ^</span>}{<span\; class="notranslate">\; =</span>}\mathrm{<span\; class="notranslate">\; GrantPermToUser</span>}<span\; class="notranslate">\; \_</span>{\mathrm{<span\; class="notranslate">\; full</span>}}^{<span\; class="notranslate">\; \&prime;</span>}$

((GrantPermToUser﹃GrantPermToUser_axiom)∧Fail))

Apply rewriting rules to the test specification and transform into Disjunctive Normal Form form. Among them, there are 8 test templates in the successful operation part, which are:

(Transition·cur-trans-class(T)=osi-class(o?)

∧ $(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧((owner(database-osi(session-database(trans-session(T))))

=trans-user(T))

∧p? ∈dbOwnerPrivs)

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok)

∨(Transition·cur-trans-class(T)=osi-class(o?)

∧ $(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧ $(\&Exists;d:\mathrm{DOMAINS}\&Center\; Dot;\mathrm{domain}-\mathrm{osi}\left(d\right)=o?)$

∧owner(o?)=trans-user(T)

∧p? ∈ dmOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok)

∨(Transition·cur-trans-class(T)=osi-class(o?)

∧ $(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧ $(\&Exists;t:\mathrm{MREAL}-\mathrm{IDS}\&CenterDot;\mathrm{real}-\mathrm{osi}\left(t\right)=o?)$

∧owner(o?)=trans-user(T)

∧p? ∈ tbOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok)

∨(Transition·cur-trans-class(T)=osi-class(o?)

∧ $(\&Exists;g:\mathrm{USERS}\&CenterDot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧ $(\&Exists;t:\mathrm{MVIEW}-\mathrm{IDS}\&Center\; Dot;\mathrm{view}-\mathrm{osi}\left(t\right)=o?)$

∧owner(o?)=trans-user(T)

∧p? ∈viOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧ re! = ok)

∨(Transition·cur-trans-class(T)=osi-class(o?)

$<span\; class="notranslate">\; \&Not;</span><span\; class="notranslate">\; (</span><span\; class="notranslate">\; \&Exists;</span>\mathrm{<span\; class="notranslate">\; g</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; USERS</span>}<span\; class="notranslate">\; \&CenterDot;</span><span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; trans</span>}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; user</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; o</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; p</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; g</span>}<span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; true</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; \&Element;</span>\mathrm{<span\; class="notranslate">\; access</span>}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; matrix</span>}<span\; class="notranslate">\; )</span>$

∧((owner(database-osi(session-database(trans-session(T))))

=trans-user(T))

∧p? ∈dbOwnerPrivs)

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok)

∨(Transition·cur-trans-class(T)=osi-class(o?)

∧ $\&Not;(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧ $(\&Exists;d:\mathrm{DOMAINS}\&CenterDot;\mathrm{domain}-\mathrm{osi}\left(d\right)=o?)$

∧owner(o?)=trans-user(T)

∧p? ∈ dmOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧ re! = ok)

∧(Transition·cur-trans-class(T)=osi-class(o?)

∧ $\&Not;(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧ $(\&Exists;t:\mathrm{MREAL}-\mathrm{IDS}\&CenterDot;\mathrm{real}-\mathrm{osi}\left(t\right)=o?)$

∧owner(o?)∈trans-user(T)

∧p? ∈ tbOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?.o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok)

∨(Transition·cur-trans-class(T)=osi-class(o?)

∧ $\&Not;(\&Exists;g:\mathrm{USERS}\&Center\; Dot;(\mathrm{trans}-\mathrm{user}\left(T\right),o?,p?,g,\mathrm{true})\&Element;\mathrm{access}-\mathrm{matrix})$

∧ $(\&Exists;t:\mathrm{MVIEW}-\mathrm{IDS}\&Center\; Dot;\mathrm{view}-\mathrm{osi}\left(t\right)=o?)$

∧owner(o?)=trans-user(T)

∧p? ∈viOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}\left(T\right),a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok)

After the fourth test template in the above example is completed, it can be expressed as follows:

$\mathrm{<span\; class="notranslate">\; test</span>}<span\; class="notranslate">\; \_</span>\mathrm{<span\; class="notranslate">\; template</span>}\mathrm{<span\; class="notranslate">\; 4</span>}\stackrel{<span\; class="notranslate">\; ^</span>}{<span\; class="notranslate">\; =</span>}<span\; class="notranslate">\; [</span>\mathrm{<span\; class="notranslate">\; signature</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; cur</span>}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; trans</span>}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; class</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; osi</span>}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; class</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; o</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; )</span>$

∧ $(\&Exists;t:\mathrm{MREAL}-\mathrm{IDS}\&CenterDot;\mathrm{real}-\mathrm{osi}\left(t\right)=o?)$

∧owner(o?)=trans-user(T)

∧p? ∈ tbOwnerPrivs

∧u? ∈ user-exists

∧ “user-adm(u?)

∧o? ∈ osi-exists

∧ $(u?,o?,p?,\mathrm{trans}-\mathrm{user}(T,)a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

∧access-matrix'=access-matrix∪{(u?, o?, p?, trans-user(T), a?)}

∧re! = ok]

The predicates in the test template can be further simplified and expressed in standard form. Next, take owner(o?)=trans-user(T) as an example to explain the refinement process.

(owner(o?)=trans-user(T))∧TCB

$<span\; class="notranslate">\; \&DoubleLeftRightArrow;</span><span\; class="notranslate">\; (</span><span\; class="notranslate">\; \&Exists;</span>\mathrm{<span\; class="notranslate">\; u</span>}\mathrm{<span\; class="notranslate">\; 1</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; USERS</span>}<span\; class="notranslate">\; \&CenterDot;</span>\mathrm{<span\; class="notranslate">\; owner</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; o</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; u</span>}\mathrm{<span\; class="notranslate">\; 1</span>}$

∧trans-user(T)=u1

∧dom owner ∈ osi_exist

∧dom tran-user ∈ tran_exist

∧ ran owner ∈ user_exist

∧ran tran-user ∈ user_exist

u1∈USERS

∧o? ∈ osi_exist

∧u1 ∈ user_exist

∧T∈tran_exist

∧owner(o?)=u1

∧trans-user(T)=u1

u1 ∈ user_exist

∧o? ∈ osi_exist

∧T∈tran_exist

The functions owner, trans-user, osi-class, cur-trans-class, user-admin, etc. in template 4 can be refined in a similar way. The standard form obtained after refining all the functions generated by test template 4 is as follows:

按语义及表达形式可以区分出操作输入应满足的约束为：According to the requirements of step 2, the template can be expressed as:

According to the semantics and expression forms, the constraints that the operation input should satisfy can be distinguished as:

∧t∈real_exist∧clss∈CLASSES∧p? ∈ tbOwnerPrivs

∧u? ∈user_exist∧u? ≠sysadmin∧u? ≠audadmin∧u? ≠secadmin

∧ $(u?,o?,p?,u1,a?)\&NotElement;\mathrm{access}-\mathrm{matrix}$

The state change caused by the operation is:

${\mathrm{<span\; class="notranslate">\; q</span>}}_{\mathrm{<span\; class="notranslate">\; 4</span>}}\stackrel{<span\; class="notranslate">\; ^</span>}{<span\; class="notranslate">\; =</span>}\mathrm{<span\; class="notranslate">\; access</span>}<span\; class="notranslate">\; -</span>{\mathrm{<span\; class="notranslate">\; matrix</span>}}^{<span\; class="notranslate">\; \&prime;</span>}<span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; access</span>}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; matrix</span>}<span\; class="notranslate">\; \&cup;</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; u</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; o</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; p</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; u</span>}\mathrm{<span\; class="notranslate">\; 1</span>}<span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; a</span>}<span\; class="notranslate">\; ?</span><span\; class="notranslate">\; )</span><span\; class="notranslate">\; \}</span>$

The output resulting from the operation is:

${\mathrm{<span\; class="notranslate">\; r</span>}}_{\mathrm{<span\; class="notranslate">\; 4</span>}}\stackrel{<span\; class="notranslate">\; ^</span>}{<span\; class="notranslate">\; =</span>}\mathrm{<span\; class="notranslate">\; re</span>}<span\; class="notranslate">\; !</span><span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; ok</span>}$

Among them, the direct input variable is: o? , p? , u? , a? , belonging to types OSI, PRIVILEGES, USERS, and BOOLEAN, respectively. The indirect input variables are: T, u1, t, clss, belonging to the types TRANSACTIONS, USERS, TUPLES and CLASSES respectively. Output variables directly: re! , indirect output variable: access-matrix.

After the operation template is determined, the division of the application type is then determined for the input variable type. where the input variable u? Indicates authorized users, of type USERS. There are three special values for this type: system administrator sysadmin, audit administrator audadmin, and security administrator secadmin. The special value division on type USERS is thus: π ₀ ={u=sysadm, u=secadm, u=audadm, u≠sysadm∧u≠Sec adm∧u≠audadm}. The number of divided blocks is four.

There are four functions on the type USERS, namely:

user-adm: USERS-|→BOOLEAN, the value field is {true, false}

user-status: USERS-|→BOOLEAN, the value range is {true, false}

user-kind: USERS-|→SKIND, the value range is {Sys, See, Aud, Common}

user-class: USERS-|→CLASSES, the special value of the value field is {SysHigh, SysLow, Trusted}.

The four function divisions on type USERS are:

π ₁ =(user-adm(u):true, user_adm(u)=false}, π ₂ ={user_status(u)=true, user-status(u)=false},

π ₃ = {user_kind(u)=sys, user_kind(u)=Sec, user_kind(u)=Aud, user_kind(u)=Common},

π ₄ = {user_class(u)=SysHigh, user_class(u)=SysLow, user_class(u)=Trusted,

user_class(u)≠SysHigh∧user_class(u)≠SysLow∧user_class(u)≠Trusted}.

The numbers of their divided blocks are 2, 2, 4, 4 respectively.

There is a collection user_exists on type USERS, and its collection is divided into ${\mathrm{\&pi;}}_5=\{u\&Element;\mathrm{user}\_\mathrm{exists},u\&NotElement;\mathrm{user}\_\mathrm{exists}\},$ The number of type divisions is 2.

Because the function user-admin in the above division has the following constraints: user-admin (sysadmin) = true, user-admin (audadmin) = true, user-admin (secadmin) = true. and

u∈user-exists ou≠sysadm∧u≠secadm∧u≠audadmuser-admin(u)=false, so dividing π ₀ and π ₁ is a subordination relationship. The comprehensive division of the two is equivalent to π ₀ .

Because the function user-status has the following constraints: user-status (sysadmin) = true, user-status (audadmin) = true, user-status (secadmin) = true. Therefore, there is a partial subordination relationship and a partial orthogonal relationship between the division of π ₀ and the division of π ₂ . The number of comprehensive divisions is 3+1×2=5. Similarly, there is a partial dependency relationship and a partial orthogonal relationship between the division of π ₀ and the division of π ₃ . The number of comprehensive divisions of (π ₀ , π ₁ , π ₂ , π ₃ ) is 3+2×4=11. The division of π ₄ and π ₀ , π ₂ , and π ₃ are all orthogonal relations, and the number of comprehensive divisions of (π ₀ , π ₁ , π ₂ , π ₃ , π ₄ ) is 11×4=44.

Due to the following restrictions on the definition domain of the above function: domuser-status=user-exists, dom user-adm=user-exists. dom user-kind=user-exists, dom user-class=user-exists. There is a subordinate relationship among π ₁ , π ₂ , π ₃ , π ₄ and π ₅ , and the number of their comprehensive divisions is 44+1=45.

Similarly, the number of integrated divisions on type PRIVILEGES is 16, the number of integrated divisions on type OSI is 4, and the number of data divisions on type BOOLEAN is 2.

Comprehensive partitioning over multiple types forms the set of input vectors. Since partitions on type PRIVILEGES are related to partitions on type OSI, the number of input vectors for the operation test_GrantPermToUser is 45*16*2=1440. In step 4, for a preset state pre_STATEi and input vector IN=(u?=alice, p?=Insert, o?=10481112, a?=true), use the tool to calculate the predicate (fest_GrantPermToUser∧pre-STATEi) [u? / alice, o? /1048l112, p? /Insert, a? /true] value. Its value is 'true', so test vectors are generated. Where the output vector OUT=(re!=ok), the state change vector $\mathrm{post}\_\mathrm{STATE}\widehat{=}\mathrm{access}-{\mathrm{matrix}}^{\&prime;}=\mathrm{access}-\mathrm{matrix}\&cup;\left\{(u?,o?,p?,u1,a?)\right\}.$ The final test vector is (IN, pre_STATEi, OUT, post_STATE).

The method provided by the present invention has been described above through specific embodiments. Those skilled in the art should understand that the present invention can be modified or equivalently replaced within the scope of not departing from the spirit and essence of the present invention.

Claims (6)

1, a kind of test example generation method of safety data base management system comprises following steps:

1) generates test specification, according to the test specification of each operation in the safe axiom requirement generation system of the formalization stipulations of descriptive system operating function and operation;

2) generate test template, test specification is carried out equivalence transformation, it is expressed as the disjunctive normal form form, thereby be one group of test template the test specification equivalent representation of operation according to certain rewriting rule;

3) type is divided, and the type that exists in the system is carried out heuristic equivalence transformation, further segments the test space of each test template representative;

4) generate test vector, subdomain is respectively tested in check, and with the exampleization, generates corresponding test vector.

2, the method for claim 1 is characterized in that, described test specification comprises:

Operate in the definition in the security of system model;

In the security of system model with the relevant safe axiom collection of operation;

The fixed constraint that exists in the relevant intermediateness variable of system.

3, the method for claim 1, it is characterized in that, the set of the test template that generates described step 2) is divided into mutually disjoint one group of test subdomain with the test space of operation, each test template is represented a test subdomain, and described test template set is complete, has covered all test spaces of tested operation.

4, the method for claim 1, it is characterized in that, described type division kind comprises one or more in the following dividing mode: preset value is divided, functional value is divided, set is divided, the data division, and the division on certain type is the comprehensive division of calculating according to above-mentioned division.

5, method as claimed in claim 4 is characterized in that, in described type partition process, if having a plurality of orthogonal division on certain type, then can divide these and use certain choice principle, reduces the test case number that is generated.

6, the method for claim 1 is characterized in that, described test vector comprises: input vector, current state vector, output vector, state variation vector.