Although static program analysis methods are frequently employed to enhance software quality,their efficiency in commercial settings is limited by their high false positive rate.The EUGENE tool can effectively lower t...Although static program analysis methods are frequently employed to enhance software quality,their efficiency in commercial settings is limited by their high false positive rate.The EUGENE tool can effectively lower the false positive rate.However,in continuous integration(CI)environments,the code is always changing,and user feedback from one version of the software cannot be applied to a subsequent version.Additionally,people find it difficult to distinguish between true positives and false positives in the analytical output.In this study,we developed the EUGENE-CI technique to address the CI problem and the EUGENE-rank lightweight heuristic algorithm to rate the reports of the analysis output in accordance with the likelihood that they are true positives.On the three projects ethereum,go-cloud,and kubernetes,we assessed our methodologies.According to the trial findings,EUGENE-CI may drastically reduce false positives while EUGENE-rank can make it much easier for users to identify the real positives among a vast number of reports.We paired our techniques with GoInsight~1 and discovered a vulnerability.We also offered a patch to the community.展开更多
Fuzzing is an effective technique to find security bugs in programs by quickly exploring the input space of programs.To further discover vulnerabilities hidden in deep execution paths,the hybrid fuzzing combines fuzzi...Fuzzing is an effective technique to find security bugs in programs by quickly exploring the input space of programs.To further discover vulnerabilities hidden in deep execution paths,the hybrid fuzzing combines fuzzing and concolic execution for going through complex branch conditions.In general,we observe that the execution path which comes across more and complex basic blocks may have a higher chance of containing a security bug.Based on this observation,we propose a hybrid fuzzing method assisted by static analysis for binary programs.The basic idea of our method is to prioritize seed inputs according to the complexity of their associated execution paths.For this purpose,we utilize static analysis to evaluate the complexity of each basic block and employ the hardware trace mechanism to dynamically extract the execution path for calculating the seed inputs’weights.The key advantage of our method is that our system can test binary programs efficiently by using the hardware trace and hybrid fuzzing.To evaluate the effectiveness of our method,we design and implement a prototype system,namely SHFuzz.The evaluation results show SHFuzz discovers more unique crashes on several real-world applications and the LAVA-M dataset when compared to the previous solutions.展开更多
A simple method is proposed, for incremental static analysis of a set of inter-colliding particles, simulating 2D flow. Within each step of proposed algorithm, the particles perform small displacements, proportional t...A simple method is proposed, for incremental static analysis of a set of inter-colliding particles, simulating 2D flow. Within each step of proposed algorithm, the particles perform small displacements, proportional to the out-of-balance forces, acting on them. Numerical experiments show that if the liquid is confined within boundaries of a set of inter-communicating vessels, then the proposed method converges to a final equilibrium state. This incremental static analysis approximates dynamic behavior with strong damping and can provide information, as a first approximation to 2D movement of a liquid. In the initial arrangement of particles, a rhombic element is proposed, which assures satisfactory incompressibility of the fluid. Based on the proposed algorithm, a simple and short computer program (a “pocket” program) has been developed, with only about 120 Fortran instructions. This program is first applied to an amount of liquid, contained in a single vessel. A coarse and refined discretization is tried. In final equilibrium state of liquid, the distribution on hydro-static pressure on vessel boundaries, obtained by proposed computational model, is found in satisfactory approximation with corresponding theoretical data. Then, an opening is formed, at the bottom of a vertical boundary of initial vessel, and the liquid is allowed to flow gradually to an adjacent vessel. Almost whole amount of liquid is transferred, from first to second vessel, except of few drops-particles, which remain, in equilibrium, at the bottom of initial vessel. In the final equilibrium state of liquid, in the second vessel, the free surface level of the liquid confirms that the proposed rhombing element assures a satisfactory incompressibility of the fluid.展开更多
The space-air-ground integrated networks(SAGINs)are pivotal for modern communication and surveillance,with a growing number of connected devices.The proliferation of Io T devices within these networks introduces new r...The space-air-ground integrated networks(SAGINs)are pivotal for modern communication and surveillance,with a growing number of connected devices.The proliferation of Io T devices within these networks introduces new risks due to potential erroneous synergistic interactions that could compromise system integrity and security.This paper addresses the challenges in coordination,synchronization,and security within SAGINs by introducing a novel static program analysis(SPA)technique using zero-knowledge(ZK)proofs.This approach ensures the detection of risky interactions without compromising sensitive source code,thus safeguarding intellectual property and privacy.The proposed method overcomes the incompatibility between SPA and ZK systems by developing an imperative programming language for SAGINs and a specialized abstract domain for interaction threats.The system translates network control algorithms into arithmetic circuits suitable for ZK analysis,maintaining high accuracy in detecting risks.Evaluations of real-world scenarios demonstrate the system's efficacy in identifying risky interactions with minimal computational overhead.This research presents the first ZK-based SPA scheme for SAGINs,enhancing security and confidentiality in network analysis while adhering to privacy regulations.展开更多
Evaluation is an essential part of the teaching process,especially in the programming course.Both students and teachers can benefit significantly from automatic program evaluation.It shortens the time required for ass...Evaluation is an essential part of the teaching process,especially in the programming course.Both students and teachers can benefit significantly from automatic program evaluation.It shortens the time required for assessment so that students can get immediate feedback.At the same time,it can also significantly reduce the workload of teachers.Currently,the automated program assessment system mainly uses a combination of static and dynamic analysis methods.The system is faced with two crucial problems of the unfinished code evaluation and the template code construction.This paper proposes a method of combining deep learning with static analysis.The syntax tree repair is used to solve the problem that the code with compiling errors cannot generate the correct syntax tree.Moreover,the target code is converted to a subset of solution space through the syntax tree standardization,which reduces the number of template code needed.Based on deep learning,the embedded token vector keeps the code’s context all the time,which ensures that the lexical-semantic remains unchanged as much as possible after the syntax tree changes.Finally,the standardized tree is represented as a vector by the recursive neural network.Cosine similarity between target and template code vectors is used as an evaluation score.The experiment shows that the similarity scores obtained by this method are consistent with the expert scores.This method can provide support for future research,such as difficult feedback and has great significance.展开更多
Worst-case execution time (WCET) analysis of multi-threaded software is still a challenge. This comes mainly from the fact that synchronization has to be taken into account. In this paper, we focus on this issue and o...Worst-case execution time (WCET) analysis of multi-threaded software is still a challenge. This comes mainly from the fact that synchronization has to be taken into account. In this paper, we focus on this issue and on automatically calculating and incorporating stalling times (e.g. caused by lock contention) in a generic graph model. The idea that thread interleavings can be studied with a matrix calculus is novel in this research area. Our sparse matrix representations of the program are manipulated using an extended Kronecker algebra. The resulting graph represents multi-threaded programs similar as CFGs do for sequential programs. With this graph model, we are able to calculate the WCET of multi-threaded concurrent programs including stalling times which are due to synchronization. We employ a generating function-based approach for setting up data flow equations which are solved by well-known elimination-based dataflow analysis methods or an off-the-shelf equation solver. The WCET of multi-threaded programs can finally be calculated with a non-linear function solver.展开更多
基金the Project"Research on the protection technology of endogenous safety for industrial control system"supported by National Science and Technology Major Project(2016YFB08002)。
文摘Although static program analysis methods are frequently employed to enhance software quality,their efficiency in commercial settings is limited by their high false positive rate.The EUGENE tool can effectively lower the false positive rate.However,in continuous integration(CI)environments,the code is always changing,and user feedback from one version of the software cannot be applied to a subsequent version.Additionally,people find it difficult to distinguish between true positives and false positives in the analytical output.In this study,we developed the EUGENE-CI technique to address the CI problem and the EUGENE-rank lightweight heuristic algorithm to rate the reports of the analysis output in accordance with the likelihood that they are true positives.On the three projects ethereum,go-cloud,and kubernetes,we assessed our methodologies.According to the trial findings,EUGENE-CI may drastically reduce false positives while EUGENE-rank can make it much easier for users to identify the real positives among a vast number of reports.We paired our techniques with GoInsight~1 and discovered a vulnerability.We also offered a patch to the community.
基金the National Key Research and Development Program of China under Grant No.2016QY07X1404National Natural Science Foundation of China(NSFC)under Grant No.61602035 and 61772078+1 种基金Beijing Science and Technology Project under Grant No.Z191100007119010,CCF-NSFOCUS Kun-Peng Scientific Research FoundationOpen Found of Key Laboratory of Network Assessment Technology,Institute of Information Engineering,Chinese Academy of Sciences.
文摘Fuzzing is an effective technique to find security bugs in programs by quickly exploring the input space of programs.To further discover vulnerabilities hidden in deep execution paths,the hybrid fuzzing combines fuzzing and concolic execution for going through complex branch conditions.In general,we observe that the execution path which comes across more and complex basic blocks may have a higher chance of containing a security bug.Based on this observation,we propose a hybrid fuzzing method assisted by static analysis for binary programs.The basic idea of our method is to prioritize seed inputs according to the complexity of their associated execution paths.For this purpose,we utilize static analysis to evaluate the complexity of each basic block and employ the hardware trace mechanism to dynamically extract the execution path for calculating the seed inputs’weights.The key advantage of our method is that our system can test binary programs efficiently by using the hardware trace and hybrid fuzzing.To evaluate the effectiveness of our method,we design and implement a prototype system,namely SHFuzz.The evaluation results show SHFuzz discovers more unique crashes on several real-world applications and the LAVA-M dataset when compared to the previous solutions.
文摘A simple method is proposed, for incremental static analysis of a set of inter-colliding particles, simulating 2D flow. Within each step of proposed algorithm, the particles perform small displacements, proportional to the out-of-balance forces, acting on them. Numerical experiments show that if the liquid is confined within boundaries of a set of inter-communicating vessels, then the proposed method converges to a final equilibrium state. This incremental static analysis approximates dynamic behavior with strong damping and can provide information, as a first approximation to 2D movement of a liquid. In the initial arrangement of particles, a rhombic element is proposed, which assures satisfactory incompressibility of the fluid. Based on the proposed algorithm, a simple and short computer program (a “pocket” program) has been developed, with only about 120 Fortran instructions. This program is first applied to an amount of liquid, contained in a single vessel. A coarse and refined discretization is tried. In final equilibrium state of liquid, the distribution on hydro-static pressure on vessel boundaries, obtained by proposed computational model, is found in satisfactory approximation with corresponding theoretical data. Then, an opening is formed, at the bottom of a vertical boundary of initial vessel, and the liquid is allowed to flow gradually to an adjacent vessel. Almost whole amount of liquid is transferred, from first to second vessel, except of few drops-particles, which remain, in equilibrium, at the bottom of initial vessel. In the final equilibrium state of liquid, in the second vessel, the free surface level of the liquid confirms that the proposed rhombing element assures a satisfactory incompressibility of the fluid.
基金supported by the National Natural Science Foundation of China(Grant Nos.62232002,62202051)the National Key R&D Program of China(Grant Nos.2021YFB2700500 and 2021YFB2700503)+7 种基金the China Postdoctoral Science Foundation(Grant Nos.2021M700435,2021TQ0042)the Guangdong Provincial Key Laboratory of Novel Security Intelligence Technologies(Grant No.2022B1212010005)the Key-Area Research and Development Program of Guangdong Province(Grant No.2021B0101400003)the Open Project Funding of Key Laboratory of Mobile Application Innovation and Governance TechnologyMinistry of Industry and Information Technology(Grant No.2023IFS080601-K)the Yunnan Provincial Major Science and Technology Special Plan Projects(Grant No.202302AD080003)the Beijing Institute of Technology Research Fund Program for Young Scholarsthe Young Elite Scientists Sponsorship Program by CAST(Grant No.2023QNRC001)
文摘The space-air-ground integrated networks(SAGINs)are pivotal for modern communication and surveillance,with a growing number of connected devices.The proliferation of Io T devices within these networks introduces new risks due to potential erroneous synergistic interactions that could compromise system integrity and security.This paper addresses the challenges in coordination,synchronization,and security within SAGINs by introducing a novel static program analysis(SPA)technique using zero-knowledge(ZK)proofs.This approach ensures the detection of risky interactions without compromising sensitive source code,thus safeguarding intellectual property and privacy.The proposed method overcomes the incompatibility between SPA and ZK systems by developing an imperative programming language for SAGINs and a specialized abstract domain for interaction threats.The system translates network control algorithms into arithmetic circuits suitable for ZK analysis,maintaining high accuracy in detecting risks.Evaluations of real-world scenarios demonstrate the system's efficacy in identifying risky interactions with minimal computational overhead.This research presents the first ZK-based SPA scheme for SAGINs,enhancing security and confidentiality in network analysis while adhering to privacy regulations.
基金supported by the 2018-2020 Higher Education Talent Training Quality and Teaching Reform Project of Sichuan Province(Grant No.JG2018-46)the Science and Technology Planning Program of Sichuan University and Luzhou(Grant No.2017CDLZG30)the Postdoctoral Science fund of Sichuan University(Grant No.2019SCU12058).
文摘Evaluation is an essential part of the teaching process,especially in the programming course.Both students and teachers can benefit significantly from automatic program evaluation.It shortens the time required for assessment so that students can get immediate feedback.At the same time,it can also significantly reduce the workload of teachers.Currently,the automated program assessment system mainly uses a combination of static and dynamic analysis methods.The system is faced with two crucial problems of the unfinished code evaluation and the template code construction.This paper proposes a method of combining deep learning with static analysis.The syntax tree repair is used to solve the problem that the code with compiling errors cannot generate the correct syntax tree.Moreover,the target code is converted to a subset of solution space through the syntax tree standardization,which reduces the number of template code needed.Based on deep learning,the embedded token vector keeps the code’s context all the time,which ensures that the lexical-semantic remains unchanged as much as possible after the syntax tree changes.Finally,the standardized tree is represented as a vector by the recursive neural network.Cosine similarity between target and template code vectors is used as an evaluation score.The experiment shows that the similarity scores obtained by this method are consistent with the expert scores.This method can provide support for future research,such as difficult feedback and has great significance.
文摘Worst-case execution time (WCET) analysis of multi-threaded software is still a challenge. This comes mainly from the fact that synchronization has to be taken into account. In this paper, we focus on this issue and on automatically calculating and incorporating stalling times (e.g. caused by lock contention) in a generic graph model. The idea that thread interleavings can be studied with a matrix calculus is novel in this research area. Our sparse matrix representations of the program are manipulated using an extended Kronecker algebra. The resulting graph represents multi-threaded programs similar as CFGs do for sequential programs. With this graph model, we are able to calculate the WCET of multi-threaded concurrent programs including stalling times which are due to synchronization. We employ a generating function-based approach for setting up data flow equations which are solved by well-known elimination-based dataflow analysis methods or an off-the-shelf equation solver. The WCET of multi-threaded programs can finally be calculated with a non-linear function solver.
