Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

Descendants of a recognizable tree language for sets of linear monadic term rewrite rules

For a tree language L and a set S of term rewrite rules over Σ, the descendant of L for S is the set S^∗(L) of trees reachable from a tree in L by rewriting in S. For a recognizable tree language L, we study the set D(L) of descendants of L for all sets of linear monadic term rewrite rules over Σ. We show that D(L) is finite. For each tree automaton A over Σ, we can effectively construct a set {R₁,…,Rk} of linear monadic term rewrite systems over Σ such that and for any 1?i<j?k, .     

Reachability Analysis over Term Rewriting Systems

This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by . An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

SQL注入攻击防御策略的研究

SQL注入攻击是Web应用中最常见的攻击,本文通过分析SQL注入攻击的原理,针对不同的攻击方法和不同的安全需求灵活使用多种防御策略堵住漏洞,如通过过滤或转义危险字符、使用正则表达式、使用URL重写技术等方法减少Web应用的风险。     

Test Sets for the Universal and Existential Closure of Regular Tree Languages

Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large. In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.     

Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions

The paper presents three formal proving methods for generalized weakly ground terminating property, i.e., weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. They can do "forward proving" by applying propositions in the proof, as well as "backward proving" by discovering lemmas during the proof.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

高性能正则表达式匹配算法评估

为对现有的高性能正则表达式匹配算法进行综合比较与分析,实现诸如DFA、D2FA、CD2FA、mDFA及XFA等最新算法,采用Snort规则集综合评估这些算法的存储空间和匹配时间。实验结果表明,在存储空间方面,与mDFA相比,XFA的存储空间减少84.9%~89.9%;在匹配效率方面,与mDFA相比,XFA的匹配时间增加了38.9%~174.6%;XFA在存储空间和匹配效率上具有良好的可伸缩性,即当规则数增加到8倍时,mDFA的存储空间增长了64倍,而XFA的存储空间仅增加了16倍,匹配时间仅增加了61.3%。     

Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings

Up to now, all existing completeness results for ordered paramodulation and Knuth–Bendix completion have required term ordering to be well founded, monotonic, and total(izable) on ground terms. For several applications, these requirements are too strong, and hence weakening them has been a well-known research challenge.Here we introduce a new completeness proof technique for ordered paramodulation where the only properties required on are well-foundedness and the subterm property. The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS).By a careful further analysis of our technique, we obtain the first Knuth–Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering whenever it exists. Note that being a reduction ordering is the minimal possible requirement on , since a TRS terminates if, and only if, it is contained in a reduction ordering.     

依赖项重写系统及其在程序设计语言中的应用

面重写系统是一种简洁通用的计算模型，在许多领域中有着重要的应用。     

Infinitary Combinatory Reduction Systems

We define infinitary Combinatory Reduction Systems (iCRSs), thus providing the first notion of infinitary higher-order rewriting. The systems defined are sufficiently general that ordinary infinitary term rewriting and infinitary λ-calculus are special cases.Furthermore, we generalise a number of known results from first-order infinitary rewriting and infinitary λ-calculus to iCRSs. In particular, for fully-extended, left-linear iCRSs we prove the well-known compression property, and for orthogonal iCRSs we prove that (1) if a set of redexes U has a complete development, then all complete developments of U end in the same term and that (2) any tiling diagram involving strongly convergent reductions S and T can be completed iff at least one of S/T and T/S is strongly convergent.We also prove an ancillary result of independent interest: a set of redexes in an orthogonal iCRS has a complete development iff the set has the so-called finite jumps property.     

Effective strategic programming for Java developers

In object programming languages, the Visitor design pattern allows separation of algorithms and data structures. When applying this pattern to tree‐like structures, programmers are always confronted with the difficulty of making their code evolve. One reason is that the code implementing the algorithm is interwound with the code implementing the traversal inside the visitor. When implementing algorithms such as data analyses or transformations, encoding the traversal directly into the algorithm turns out to be cumbersome as this type of algorithm only focuses on a small part of the data‐structure model (e.g., program optimization). Unfortunately, typed programming languages like Java do not offer simple solutions for expressing generic traversals. Rewrite‐based languages like ELAN or Stratego have introduced the notion of strategies to express both generic traversal and rule application control in a declarative way. Starting from this approach, our goal was to make the notion of strategic programming available in a widely used language such as Java and thus to offer generic traversals in typed Java structures. In this paper, we present the strategy language SL that provides programming support for strategies in Java. Copyright © 2012 John Wiley & Sons, Ltd.     

Practical ultra‐reliability for abstract data types

The Term Redundancy Method (TRM) is a novel approach for obtaining ultra‐reliable programs through specification‐based testing. Current specification‐based testing schemes need a prohibitively large number of test cases for estimating ultra‐reliability. They assume the availability of an accurate program‐usage distribution prior to testing, and they assume the availability of a test oracle. This paper shows how to obtain ultra‐reliable abstract data types specified with equational specifications, with a practical number of test cases, without an accurate usage distribution, and without the usual test oracle. The effectiveness of the TRM in failure detection and recovery is demonstrated on the aircraft collision avoidance system TCAS. Copyright © 2007 John Wiley & Sons, Ltd.     

面向不平衡数据集的机器学习分类策略

由于不平衡数据集的内在固有特性,使得分类结果常受数量较多的类别影响,造成分类性能下降。近年来,为了能够从类别不平衡的数据集中学习数据的内在规律并且挖掘其潜在的价值,提出了一系列基于提升不平衡数据集机器学习分类算法准确率的研究策略。这些策略主要是立足于数据层面、分类模型改进层面来解决不平衡数据集分类难的困扰。从以上两个方面论述面向不平衡数据集分类问题的机器学习分类策略,分析和讨论了针对不平衡数据集机器学习分类器的评价指标,总结了不平衡数据集分类尚存在的问题,展望了未来能够深入研究的方向。特别的,这些讨论的研究主要关注类别极端不平衡场景下的二分类问题所面临的困难。     

Smoothness of Boundaries of Regular Sets

We prove that the boundary of an r-regular set is a codimension one manifold of class C ¹.     

General Algorithms for Permutations in Equational Inference

Mechanized systems for equational inference often produce many terms that are permutations of one another. We propose to gain efficiency by dealing with such sets of terms in a uniform manner, by the use of efficient general algorithms on permutation groups. We show how permutation groups arise naturally in equational inference problems, and study some of their properties. We also study some general algorithms for processing permutations and permutation groups, and consider their application to equational reasoning and term-rewriting systems. Finally, we show how these techniques can be incorproated into resolution theorem-proving strategies.     

Mechanizing and Improving Dependency Pairs

The dependency pair technique is a powerful method for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by well-founded orders. We improve the dependency pair technique by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs that simplify (innermost) termination proofs significantly. To fully mechanize the approach, we show how transformations and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples. Supported by the Deutsche Forschungsgemeinschaft DFG, grant GI 274/5-1.     

基于正则表达式的语音识别控制策略研究

文中提出一种新型控制策略,把正则表达式和服务机器人的语音控制结合起来,前者利用预定义的正则表达式对语音识别内容进行模式检出,后者根据检出的模式对机器人进行策略控制。通过分析识别文本构建正则表达式,使用微软SAPI构建客户端语音引擎进行语音识别,在服务机器人平台上验证策略的有效性、实用性和快速性。该新型控制策略把正则表达式应用在语音识别控制策略中,使语音交互技术将人类之间的交流方式应用于人类与机器之间。使机器人用正则表达式对人类语言进行词法分析实现自然语言的理解。提出的方法使机器人能够“理解”同一个语音命令的多种表达方式,使服务机器人的语音识别控制策略更具柔性和自然性,具有重要的应用价值和应用前景。     

必要平行最外归约策略

在必要集、必要位置等概念基础上，定义了必要平行最外归约策略．基于最小化必要集思想，该策略适用于正则系统全集，并接近按需调用策略的效率，在适用范围、效率和可实现性三个方面得到了兼顾．