Research On RUST Testing Tools Integrating Fuzzing And Formal Verification

Formal Verification Rust language is a new kind of programming language that takes both safety and efficiency into account.Nearly 70% of computer vulnerabilities come from memory problems,and Rust language almost eliminates such problems.This feature makes Rust language a very suitable tool for the development of a series of system softwares.As the Rust language matures,it has gradually attracted widespread attention in the field of industry: Microsoft has applied it to the development of key components,while hundreds of other well-known domestic and foreign companies,such as Amazon,Google,and Ant Financial,have also begun to take Rust language into practice.To meet the security requirements of users;in addition,the scientific research community has also developed a strong interest in the Rust language: since2017,Rust language has been on the top of the "Most Popular Programming Language" list on the Stack Overflow forum for five times.The soar increase of Rust files has also brought new demands: the vast majority of Rust language users regard safety as the first criterion for programming,and they hope that Rust language will make greater progress in the future,and the safety of Rust programs can be further improved-however,given the current circumstances,it is unlikely that Rust language will make a significant leap in the short term.If developers have higher requirements for the security of Rust programs,the most reasonable solution is to use automated testing tools to test their programs.However,as a young language with excellent security,the field of Rust language testing tools is almost empty.At present,the domestic Rust research field has not proposed corresponding test tools;foreign Rust test tools are poor in quantity and technology:these tools are basically built on the technology migration of mature test tools.Among them,the authors of the Seer tool and the Seahorn tool have modified their mature testing tools to support the Rust language.In the field of software testing,the combination of dynamic symbolic execution technology and fuzzing technology has achieved good performance in C++ and Python programs.Fuzzing generates a large number of test cases that trigger bugs in the target program.The dynamic symbolic execution technology finds errors by exploring the program path.It uses the instrumentation technology to obtain the constraint information of the path,and generates test cases corresponding to each program path.The two technologies are combined in the well-known Driller tool and show great potential.However,there is currently a lack of similar testing tools in Rust In view of this,thus,this article will conduct some preliminary explorations in this field.The contributions of this paper are as follows:First,it introduces the current status of the combination of fuzzing and dynamic symbolic execution technology,and proposes a design scheme to improve such technology to test Rust language programs.Second,it build a Rust testing tool,Veri Rust,based on the method proposed above.Veri Rust,which generates large amounts of input through the AFL fuzzing tool,quickly finds compartmentalized parts of the program.At the same time,the LLVM technology is used to translate the Rust program into the intermediate statement IR.When the fuzzing tool fails,the KLEE dynamic symbolic execution tool,which is reintegrated for the Rust language,is used to find the input that can pass the complex inspection on the intermediate statement.Third,experiments were conducted on the datasets composed of the two most frequently used third-party libraries in Rust,serde?json and url.The experimental results show that,on top of the most commonly used third-party libraries in Rust,the tool proposed in this paper can achieve high code coverage and fully detect program errors.This reflects a considerable degree of feasibility,effectiveness and practicality.It is further proved that the tools that combine formal verification in the hardware industry,fuzzing technology in software testing and LLVM intermediate language conversion can be migrated to the field of Rust language testing.And this kind of tool shows high coverage and accuracy in Rust combat,and the subsequent development value is guaranteed.In summary,the work in this paper has achieved a valuable preliminary exploration of the Rust language field.