CN-116185829-B - Symbolized memory mapping method and system

CN116185829BCN 116185829 BCN116185829 BCN 116185829BCN-116185829-B

Abstract

The invention discloses a symbolized memory mapping method and system, the method comprises the steps of S1, initializing a memory attribute judging device according to memory read-write attribute configuration, S2, initializing a symbolized expression mapping device according to symbolized memory configuration, S3, receiving read operation or write operation by an input processor, judging validity of the read-write operation by the memory attribute judging device according to the memory attribute judging device in the S1, for illegal operation, giving output to an output processor, for legal operation, giving subsequent operation to the symbolized expression mapping device, S4, processing the read-write operation of symbolized memory according to the read-write operation and symbolized memory configuration in the S2 by the symbolized expression mapping device according to conditions. The system is used for implementing the method. The invention has the advantages of simple principle, wide application range, small hardware cost and the like.

Inventors

YU BO
XU BINBIN
WANG BAOSHENG
CHEN SHUHUI
YANG QIANG
LIU RUNHAO

Assignees

中国人民解放军国防科技大学

Dates

Publication Date: 20260508
Application Date: 20221220

Claims (9)

1. A method for symbolized memory mapping, comprising: Step S1, initializing a memory attribute judging device according to memory read-write attribute configuration; s2, initializing a symbol expression mapper according to the symbolized memory configuration; step S3, the input processor receives the read operation or the write operation, the memory attribute judging device judges the validity of the read operation and the write operation according to the memory attribute judgment in the step S1, and the output processor is given out to generate output for illegal operation; Step S4, the symbol expression mapper processes the read-write operation of the symbolized memory according to the read-write operation and the symbolized memory configuration in the step S2 according to the situation; the symbolized memory is divided into a readable memory, a writable memory and a readable and writable memory, and the reading and writing operations of the memory are processed according to the following conditions: (1) For the case of reading from the unsigned memory, if the content is a symbolic expression, a symbolic expression is returned, and if the content is a non-symbolic expression, a specific value is returned; (2) For writing to the unsigned memory, if the written value is a symbolic expression, the memory is mapped to the symbolic expression, and if the written value is a non-symbolic expression, the memory is ignored; (3) For the case of reading from the symbolized memory, if the content is a symbolized expression, returning the symbolized expression, and if the content is a non-symbolized expression, returning the symbolized expression corresponding to the specific value; (4) For the case of writing to symbolized memory, then the record memory maps to a symbolic expression.
2. The method of claim 1, wherein the step S4 includes the steps of, for a read operation, if the read memory ra1 is configured as a symbolic memory, giving the symbolic expression to the output processor for outputting if the read memory is mapped to the symbolic expression sym_ra1, otherwise, generating the symbolic expression sym_ra1_value according to the specific memory value ra1_value of the read memory, and giving the symbolic expression to the output processor for outputting.
3. The method of claim 1, wherein the step S4 includes reading the memory ra2 without being configured as a symbolic memory, and if the read memory is mapped to the symbolic expression sym_ra2, giving the symbolic expression to the output processor for outputting, otherwise giving the specific memory value ra2_value of the read memory to the output processor for outputting.
4. The method of claim 1, wherein the step S4 includes, for a write operation, when the written memory wa1 is configured as a symbolic memory, generating a symbol value sym_wa1_value according to a specific value wa1_value if the written memory is the specific value, directly using the symbol value sym_wa1_value if the written memory is the symbol value sym_wa1_value, and then recording a mapping from the written memory wa1 to the symbol expression sym_wa1_value in the symbol expression, and delivering the symbol expression sym_wa1_value to the output processor for output.
5. The method of claim 1, wherein the step S4 includes writing, if the written memory wa2 is not configured as a symbolic memory, recording a mapping from the written memory wa2 to the symbolic expression sym_wa2_value in the symbolic expression if the written memory value is the symbolic value sym_wa2_value, and delivering the symbolic expression sym_wa2_value to the output processor for output, and delivering the specific value wa2_value to the output processor for output if the written memory value is the specific value wa2_value.
6. The symbolized memory mapping method according to any one of claims 1 to 5, wherein in step S1, the memory read-write attribute configuration describes a section of memory range read-only r or read-write rw, and is expressed in json format syntax.
7. The method according to any one of claims 1-5, wherein in step S2, the symbolic memory allocation describes a segment of symbolic memory range, and the symbolic memory allocation is represented by a json format syntax.
8. The symbolized memory mapping system is characterized by comprising a memory attribute judging device, a symbolized expression mapping device, an input processor and an output processor, wherein the input processor is used for receiving a read operation or a write operation, the memory attribute judging device is used for judging the validity of the read operation or the write operation; the symbolized memory is divided into a readable memory, a writable memory and a readable and writable memory, and the reading and writing operations of the memory are processed according to the following conditions: (1) For the case of reading from the unsigned memory, if the content is a symbolic expression, a symbolic expression is returned, and if the content is a non-symbolic expression, a specific value is returned; (2) For writing to the unsigned memory, if the written value is a symbolic expression, the memory is mapped to the symbolic expression, and if the written value is a non-symbolic expression, the memory is ignored; (3) For the case of reading from the symbolized memory, if the content is a symbolized expression, returning the symbolized expression, and if the content is a non-symbolized expression, returning the symbolized expression corresponding to the specific value; (4) For the case of writing to symbolized memory, then the record memory maps to a symbolic expression.
9. The symbolized memory mapping system of claim 8 wherein the memory read-write attribute configuration describes a segment of memory range read-only r or read-write rw in json format syntax, and the symbolized memory configuration describes a segment of symbolized memory range in json format syntax.

Description

Symbolized memory mapping method and system Technical Field The invention mainly relates to the technical field of computer program analysis, in particular to a symbolized memory mapping method and a symbolized memory mapping system. Background "Symbolic execution" is a program analysis technique in the field of computer science, which is a technique of analyzing a program by using abstract symbolic values instead of concrete values as variables of the program. When a program is analyzed using symbolic execution, the program will use the symbolic value as input, rather than the specific value used when the program is executed generally. When the target code is reached, the analyzer may get the corresponding path constraint and then solve for the specific value that may trigger the target code through the constraint solver. The process of symbol execution involves the maintenance of a program memory space, which requires the establishment of a mapping of the program memory space to the symbol expression. Symbolized memory mapping methods are an integral part of both source code and symbolic execution of binary programs. However, the existing symbolized memory mapping method still has some disadvantages: (1) The read-write attribute of the memory is not maintained; (2) If all memories used by the program are symbolized, the expenditure is high; (3) If a part of the memory used by the program is symbolized, the symbol expression read from the unsigned memory is null or a specific value. Disclosure of Invention The technical problem to be solved by the invention is to provide the symbolized memory mapping method and the symbolized memory mapping system which are simple in principle, wide in application range and low in hardware cost aiming at the technical problem existing in the prior art. In order to solve the technical problems, the invention adopts the following technical scheme: A method of symbolizing a memory mapping, comprising: Step S1, initializing a memory attribute judging device according to memory read-write attribute configuration; s2, initializing a symbol expression mapper according to the symbolized memory configuration; step S3, the input processor receives a read operation or a write operation, and the memory attribute judging device judges the validity of the read operation and the write operation according to the memory attribute judging device in the step S1; and S4, the symbol expression mapper processes the read-write operation of the symbolized memory according to the read-write operation and the symbolized memory configuration in the step S2. The step S4 includes that under the condition that the read memory ra1 is configured as a symbolized memory for read operation, if the read memory is mapped to the symbolized expression sym_ra1, the symbolized expression is given to an output processor for output, otherwise, the symbolized expression sym_ra1_value is generated according to the specific memory value ra1_value of the read memory and is given to the output processor for output. In step S4, if the read memory ra2 is not configured as a symbolized memory, if the read memory is mapped to the symbolized expression sym_ra2, the symbolized expression is given to the output processor for output, otherwise, the specific memory value ra2_value of the read memory is given to the output processor for output. As a further improvement of the method, the step S4 comprises the steps of for writing, generating a symbol value sym_wa1_value according to a specific value wa1_value if the written memory is configured as a symbolized memory, directly using the symbol value sym_wa1_value if the written memory is the symbol value sym_wa1_value, recording the mapping from the written memory wa1 to the symbol expression sym_wa1_value in the symbol expression, and delivering the symbol expression sym_wa1_value to an output processor for output. As a further improvement of the method, the step S4 comprises the steps of for writing, if the written memory wa2 is not configured as a symbolized memory, if the value of the written memory is a symbol value sym_wa2_value, recording the mapping from the written memory wa2 to the symbol expression sym_wa2_value in the symbol expression, and giving the symbol expression sym_wa2_value to an output processor for output, and if the value of the written memory is a specific value wa2_value, giving the specific value wa2_value to the output processor for output. In the step S1, the memory read-write attribute configuration describes a section of memory range read-only r or read-write rw, and adopts the syntax representation of json format. As a further improvement of the method of the present invention, in the step S2, the symbolic memory configuration describes a segment of the symbolic memory range, and the symbolic memory range is expressed by adopting a syntax of json format. The invention further provides a symbolized memory mapping system which comprises a memory attr