A new term has been added to this issue: Satisfiability modulo theories.
Opening Remarks:
A new term has been added to this issue: Satisfiability modulo theories. Satisfiability modular theory refers to the problem of determining the satiety of predicate logic formulas that are interpreted in background theory by functions and relational symbols.
Satisfiability modulo theories
Author: Wu Zhilin, Ma Feifei, Cai Shaowei (Institute of Software, Chinese Academy of Sciences)
InfoBox：
Chinese: The Theory of The Satisfiability Mold
Foreign name: Satisfiability modulo theories
Abbreviation: SMT
Discipline: Computer Software and Theory
Basic Introduction:
The basic idea of satisfiability modal theory is to propose a general framework for multiple data types and corresponding predicate logic theory, so that the satisfiability determination problem of predicate logic formulas under specific background theory can be solved, and further, the satisfiability determination problem of mixed logic formulas covering multiple theories can be solved. Satisfiability modal theory can handle fewer logical formulas than interactive theorem proofs, generally considering predicate logic formulas with immeasurable words or less nested quantifiers, but its advantage is that it can fully automate logical reasoning.
The theory of predicate logic considered by the satiety modulo theory mainly includes unexplained functions (EUFs), bit vectors (BV), arrays (Arrays), integer linear arithmetic (LIA), real linear arithmetic (LRA), integer nonlinear arithmetic (NIA), strings (String), etc. The tool for solving the SMT formula satisfiability problem is called the SMT solver. At present, the more representative SMT solvers include the Z3 solver developed by Microsoft, the CVC4/CVC5 solver developed by Stanford University and the University of Iowa, and the Yes solver developed by the Stanford International Research Institute. The study of SMT solving is not only the subject of IJCAR/CADE, CP and SAT, but also an important international conference in the field of formal verification and programming languages, CAV, POPL, FM, and TACAS. SMT is also highly concerned by the industry, and the research institutes or laboratories of Microsoft, Intel, Amazon, Cadence and other companies are carrying out research projects related to SMT.
History:
Realizing the automation of logical reasoning is one of the ultimate dreams of human society, which runs through the development process of human civilization. In the 1950s and 1960s, the semiotic school of artificial intelligence explored the automation of logical reasoning and developed a number of logical reasoning systems [1,2,3,4], but the reasoning ability of these systems was generally weak. Around 2000, a breakthrough was made in solving the satisfiability problem (SAT) of propositional logic, and Princeton University's Sharad Malik team developed the SAT solver Chaff[5], which first realized the solution of large-scale propositional logic formulas and began to be applied to industrial solutions to practical problems. Almost at the same time, the study of decision algorithms for various special logic theories began to revive, and a number of early solvers appeared, such as SVC[6] and Step[7] of Stanford University, AND THE ICS [8] of SRI. The researchers then considered the fusion of SAT and special theoretical determination algorithms to propose the satisfiability modulus theory problem (SMT) [9]. Milestones in the development of SMT include the initiation of the annual SMT Workshop in 2003,[10] the introduction of SMT-LIB as an input format standard for solving SMT problems in 2004,[11] and the creation of the SMT-COMP competition in 2005. To date, the SMT competition has collected more than 100,000 test cases. After 2010, a number of more mature SMT solvers appeared, such as Microsoft Z3[13] in the United States, CVC4/CVC5 at Stanford University and the University of Iowa [14,15], and Yeses [16] at the Stanford Institute of International Studies in the United States.
Fields of application:
The SMT solver has become the basic engine in the fields of software engineering, programming languages, and information security, and its application scenarios are diverse, and these application scenarios are described in detail below.
Software Analysis and Validation:
Software deductive verification boils down to the implication problem of two logical formulas, which can then be encoded as the satisfaction problem of SMT to solve. Microsoft developed program deductive verification tools Dafny[17] and Boogie based on the Z3 solver.
The symbolic execution of the software encodes path constraints into SMT formulas, thereby encoding path feasibility questions as SMT problems, and if the SMT formula has a solution, test cases can be generated. Stanford University developed the symbolic execution tool Klee based on the SMT solver,[19] and Microsoft developed the test case generation tool Pex based on the Z3 solver.
The basic idea of the synth problem is to encode the procedural synthesis problem into an SMT formula and use the SMT solver to search for a program that meets the requirements[21].
Software fuzz testing is a very popular technology for finding vulnerabilities in software systems in the past decade, black box fuzz testing based on dynamic execution has the problem of low coverage, so researchers have proposed white box fuzz testing, that is, the combination of symbol execution and dynamic execution to find more vulnerabilities, and the SMT solver is the core of symbol execution, so white box fuzz testing technology widely uses SMT solvers. Microsoft developed SAGE, a fuzz testing tool based on the Z3 solver,[22] and found many vulnerabilities in Windows applications.
Proof of theorem: SMT solvers have been integrated into many interactive theorem provers such as Coq and Isabelle to increase their automation .[23,24]
Cloud Computing Security: Amazon Web Services established an automated inference group, based on the SMT solver, developed the Zelkova tool, where the former is used to verify the security of AMS identity and key management policies and simple storage service configuration policies, and the latter is used to verify cryptographic algorithms to achieve security in side-channel attacks.
bibliography:
[1] Allen Newell, Herbert A. Simon: The logic theory machine-A complex information processing system. IRE Trans. Inf. Theory 2(3): 61-79 (1956)
[2] Allen Newell, J. C. Shaw, Herbert A. Simon: Empirical explorations of the logic theory machine: a case study in heuristic. IRE-AIEE-ACM Computer Conference (Western) 1957: 218-230.
[3] Allen Newell, J. C. Shaw: Programming the logic theory machine. IRE-AIEE-ACM Computer Conference (Western) 1957: 230-240.
[4] John Alan Robinson: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12(1): 23-41 (1965)
[5] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver. DAC 2001: 530-535.
[6] Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt: A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37.
[7] Zohar Manna, Nikolaj Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Luca de Alfaro, Harish Devarajan, Arjun Kapur, Jaejin Lee, Henny Sipma, Tomás E. Uribe: STeP: The Stanford Temporal Prover. TAPSOFT 1995: 793-794.
[8] Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar: ICS: Integrated Canonizer and Solver. CAV 2001: 246-249.
[9] Cesare Tinelli: A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. JELIA 2002: 308-319.
[10] http://smt-workshop.cs.uiowa.edu/
[11] http://smtlib.cs.uiowa.edu/
[12] https://smt-comp.github.io/
[13] https://github.com/Z3Prover/z3
[14] https://cvc4.github.io/
[15] https://github.com/cvc5
[16] https://yices.csl.sri.com/
[17] https://github.com/dafny-lang/dafny
[18] https://github.com/boogie-org/boogie
[19] https://klee.github.io/
[20] http://duderino.github.io/injection/PexAndMoles.html
[21] https://sygus.org/
[22] Patrice Godefroid, Michael Y. Levin, David A. Molnar: Automated Whitebox Fuzz Testing. NDSS 2008.
[23] https://smtcoq.github.io/
[24] Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson: Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013).
[25] https://aws.amazon.com/cn/blogs/security/tag/automated-reasoning/
Introduction to the Terminology Working Committee and terminology platform:
The main function of the Committee on Terminology is to collect, translate, interpret, validate and recommend computer terms and promote them on the CCF platform. This is of great significance for clarifying the disciplinary system, carrying out scientific research, and widely disseminating science and knowledge in the whole society.
The construction and continuous optimization of the terminology crowdsourcing platform CCFpedia can effectively promote the collection, approval, standardization and dissemination of Chinese computer terminology, and at the same time play a role in promoting the customization of standardized standards in various fields.
The new version of CCFpedia Computer Terminology Platform (http://term.ccf.org.cn) integrates the editing and operation of terminology with browsing and use, abandons the tedious steps of cross-platform operation in the old version, and upgrades the interface observability, allowing users to easily and conveniently access terminology information. At the same time, the new version of the platform introduces the knowledge graph to organize all terminology data, and upgrades the application form of terminology browsing through the multi-layer association of the graph.
Working Committee on the Validation of Computer Terminology
director:
Ting Liu (Harbin Institute of Technology)
Deputy Director:
Haofen Wang (Tongji University)
Guoliang Li (Tsinghua University)
Assistant Director:
Li Yibin (Shanghai Haiqizhi Information Technology Co., Ltd.)
Executive Committee:
Ding Jun (Shanghai Haiqizhi Information Technology Co., Ltd.)
Lin Junyu (Institute of Information Engineering, Chinese Academy of Sciences)
Lan Yanyan (Tsinghua University)
Weinan Zhang (Harbin Institute of Technology)
