Digital Library[ Search Result ]
An effective Seed Selection Method for Maximizing the Performance of Symbolic Execution
http://doi.org/10.5626/JOK.2025.52.7.578
Symbolic execution is a promising software testing technique that aims to maximize the coverage of executed code areas of program under test by effectively generating test cases. A well-known challenge in symbolic execution is the high cost associated with solving path conditions. One solution to this challenge is to utilize generated test cases as seed inputs for a symbolic execution tool, thereby reducing the number of required solver calls. The effectiveness of this solution depends on the selection of appropriate test cases as seed inputs. This paper proposes a method to enhance the performance of symbolic execution by grouping the generated test cases into clusters, identifying the most promising cluster and selecting the most potential seed input from within it. Experimentally, the proposed method achieved 42.0% more branch coverage on average than traditional symbolic execution tools without seed inputs.
Extracting Instruction Set Architecture Semantics from a Processor Register-transfer Level
http://doi.org/10.5626/JOK.2023.50.10.827
Domain-specific processors have specialized instructions tailored for frequently used operations in a particular domain, which enables them to achieve higher performance. This presents a challenge for program analysis, as the specialized instructions make it difficult to formally describe the instruction semantics. To address this, we present SemTracter, a tool that automatically extracts instruction semantics from a processor implemented in a hardware description language (HDL) at the register-transfer level (RTL). SemTracter obtains the semantics by simulating the processor RTL symbolically and compiling the results into formal instruction semantics using the Sail language. Our evaluation of the SemTracter on a small RISC-V processor RTL showed that it was able to extract the semantics of basic instructions from a 5-stage processor. Most of the RISC-V 32-bit integer base user-level ISA (RV32I) instructions were extracted and the generated semantics matched the manually written version.
Automated Unit-test Generation for Detecting Vulnerabilities of Android Kernel Modules
In this study, we propose an automated unit test generation technique for detecting vulnerabilities of Android kernel modules. The technique automatically generates unit test drivers/stubs and unit test inputs for each function of Android kernel modules by utilizing dynamic symbolic execution. To reduce false alarms caused by function pointers and missing pre-conditions of automated unit test generation technique, we develop false alarm reduction techniques that match function pointers by utilizing static analysis and generate pre-conditions by utilizing def-use analysis. We showed that the proposed technique could detect all existing vulnerabilities in the three modules of Android kernel 3.4. Also, the false alarm reduction techniques removed 44.9% of false alarms on average.
Effective Integer Promotion Bug Detection Technique for Embedded Software
Yunho Kim, Taejin Kim, Moonzoo Kim, Ho-jung Lee, Hoon Jang, Mingyu Park
C compilers for 8-bit MCUs used in washing machines and refrigerators often do not follow the C standard to improve runtime performance. Developers who are unaware of the difference between C compilers following the C standard and the C compilers for 8-bit MCU can cause bugs that do not appear in the standard C environment but appear in the embedded systems using 8-bit MCUs. It is difficult for bug detectors that assume the standard C environment to detect such bugs. In this paper, we introduce integer promotion bugs caused by the different integer promotion rules of the C compilers for 8-bit MCU from the C standard and propose 5 bug patterns where the integer promotion bugs occur. We have developed an integer promotion bug detection tool and applied it to the washing machine control software developed by the LG electronics. The integer promotion bug detection tool successfully detected 27 integer promotion bugs in the washing machine control software.
Search
Journal of KIISE
- ISSN : 2383-630X(Print)
- ISSN : 2383-6296(Electronic)
- KCI Accredited Journal
Editorial Office
- Tel. +82-2-588-9240
- Fax. +82-2-521-1352
- E-mail. chwoo@kiise.or.kr