Searcharxiv⌕ Search

arXiv subjects

Taolue Chen

Publications and source records attributed to Taolue Chen.

At least 55 records · Page 3Linked to original sources

Adversarial Robustness of Deep Code Comment Generation

Deep neural networks (DNNs) have shown remarkable performance in a variety of domains such as computer vision, speech recognition, or natural language processing. Recently they also have been applied to various software engineering tasks, typically involving processing source code. DNNs are well-known to be vulnerable to adversarial examples, i.e., fabricated inputs that could lead to various misbehaviors of the DNN model while being perceived as benign by humans. In this paper, we focus on the code comment generation task in software engineering and study the robustness issue of the DNNs when they are applied to this task. We propose ACCENT, an identifier substitution approach to craft adversarial code snippets, which are syntactically correct and semantically close to the original code snippet, but may mislead the DNNs to produce completely irrelevant code comments. In order to improve the robustness, ACCENT also incorporates a novel training method, which can be applied to existing code comment generation models. We conduct comprehensive experiments to evaluate our approach by attacking the mainstream encoder-decoder architectures on two large-scale publicly available datasets. The results show that ACCENT efficiently produces stable attacks with functionality-preserving adversarial examples, and the generated examples have better transferability compared with baselines. We also confirm, via experiments, the effectiveness in improving model robustness with our training method.

cs.SE↗

Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables

Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provide such a support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods in both precision and efficiency.

cs.PL↗

BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks

Verifying and explaining the behavior of neural networks is becoming increasingly important, especially when they are deployed in safety-critical applications. In this paper, we study verification problems for Binarized Neural Networks (BNNs), the 1-bit quantization of general real-numbered neural networks. Our approach is to encode BNNs into Binary Decision Diagrams (BDDs), which is done by exploiting the internal structure of the BNNs. In particular, we translate the input-output relation of blocks in BNNs to cardinality constraints which are then encoded by BDDs. Based on the encoding, we develop a quantitative verification framework for BNNs where precise and comprehensive analysis of BNNs can be performed. We demonstrate the application of our framework by providing quantitative robustness analysis and interpretability for BNNs. We implement a prototype tool BDD4BNN and carry out extensive experiments which confirm the effectiveness and efficiency of our approach.

cs.LG↗

Boosting API Recommendation with Implicit Feedback

Developers often need to use appropriate APIs to program efficiently, but it is usually a difficult task to identify the exact one they need from a vast of candidates. To ease the burden, a multitude of API recommendation approaches have been proposed. However, most of the currently available API recommenders do not support the effective integration of users' feedback into the recommendation loop. In this paper, we propose a framework, BRAID (Boosting RecommendAtion with Implicit FeeDback), which leverages learning-to-rank and active learning techniques to boost recommendation performance. By exploiting users' feedback information, we train a learning-to-rank model to re-rank the recommendation results. In addition, we speed up the feedback learning process with active learning. Existing query-based API recommendation approaches can be plugged into BRAID. We select three state-of-the-art API recommendation approaches as baselines to demonstrate the performance enhancement of BRAID measured by Hit@k (Top-k), MAP, and MRR. Empirical experiments show that, with acceptable overheads, the recommendation performance improves steadily and substantially with the increasing percentage of feedback data, comparing with the baselines.

cs.SE↗

Online Observability of Boolean Control Networks

Observabililty is an important topic of Boolean control networks (BCNs). In this paper, we propose a new type of observability named online observability to present the sufficient and necessary condition of determining the initial states of BCNs, when their initial states cannot be reset. And we design an algorithm to decide whether a BCN has the online observability. Moreover, we prove that a BCN is identifiable iff it satisfies controllability and the online observability, which reveals the essence of identification problem of BCNs.

eess.SY↗

Learning Safe Neural Network Controllers with Barrier Certificates

We provide a novel approach to synthesize controllers for nonlinear continuous dynamical systems with control against safety properties. The controllers are based on neural networks (NNs). To certify the safety property we utilize barrier functions, which are represented by NNs as well. We train the controller-NN and barrier-NN simultaneously, achieving a verification-in-the-loop synthesis. We provide a prototype tool nncontroller with a number of case studies. The experiment results confirm the feasibility and efficacy of our approach.

eess.SY↗

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths of, or positions in, strings. Analysis and testing of string-manipulating programs can be formulated as the path feasibility problem: given a symbolic execution path, does there exist an assignment to the inputs that yields a concrete execution that realizes this path? Such a problem can naturally be reformulated as a string constraint solving problem. Although state-of-the-art string constraint solvers usually provide support for both string and integer data types, they mainly resort to heuristics without completeness guarantees. In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers.

cs.LO↗

A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs

Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, in this article, we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. We then give novel model-counting based and pattern-matching based methods which are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious. We evaluate our approach on various implementations of arithmetic cryptographicprograms.The experiments confirm that our approach out performs the state-of-the-art base lines in terms of applicability, accuracy and efficiency.

cs.CR↗

Finger Texture Biometric Characteristic: a Survey

\begin{abstract} In recent years, the Finger Texture (FT) has attracted considerable attention as a biometric characteristic. It can provide efficient human recognition performance, because it has different human-specific features of apparent lines, wrinkles and ridges distributed along the inner surface of all fingers. Also, such pattern structures are reliable, unique and remain stable throughout a human's life. Efficient biometric systems can be established based only on FTs. In this paper, a comprehensive survey of the relevant FT studies is presented. We also summarise the main drawbacks and obstacles of employing the FT as a biometric characteristic, and provide useful suggestions to further improve the work on FT. \end{abstract}

cs.CV↗

User Review-Based Change File Localization for Mobile Applications

In the current mobile app development, novel and emerging DevOps practices (e.g., Continuous Delivery, Integration, and user feedback analysis) and tools are becoming more widespread. For instance, the integration of user feedback (provided in the form of user reviews) in the software release cycle represents a valuable asset for the maintenance and evolution of mobile apps. To fully make use of these assets, it is highly desirable for developers to establish semantic links between the user reviews and the software artefacts to be changed (e.g., source code and documentation), and thus to localize the potential files to change for addressing the user feedback. In this paper, we propose RISING (Review Integration via claSsification, clusterIng, and linkiNG), an automated approach to support the continuous integration of user feedback via classification, clustering, and linking of user reviews. RISING leverages domain-specific constraint information and semi-supervised learning to group user reviews into multiple fine-grained clusters concerning similar users' requests. Then, by combining the textual information from both commit messages and source code, it automatically localizes potential change files to accommodate the users' requests. Our empirical studies demonstrate that the proposed approach outperforms the state-of-the-art baseline work in terms of clustering and localization accuracy, and thus produces more reliable results.

cs.SE↗

Model-based Automated Testing of JavaScript Web Applications via Longer Test Sequences

JavaScript has become one of the most widely used languages for Web development. However, it is challenging to ensure the correctness and reliability of Web applications written in JavaScript, due to their dynamic and event-driven features. A variety of dynamic analysis techniques for JavaScript Web applications have been proposed, but they are limited in either coverage or scalability. In this paper, we propose a model-based automated approach to achieve high code coverage in a reasonable amount of time via testing with longer event sequences. We implement our approach as the tool LJS, and perform extensive experiments on 21 publicly available benchmarks (18,559 lines of code in total). On average, LJS achieves 86.4\% line coverage in 10 minutes, which is 5.4\% higher than that of JSDep, a breadth-first search based automated testing tool enriched with partial order reduction. In particular, on large applications, the coverage of LJS is 11-18\% higher than that of JSDep. Our empirical finding supports that longer test sequences can achieve higher code coverage in JavsScript testing.

cs.SE↗

Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks

Power side-channel attacks, which can deduce secret data via statistical analysis, have become a serious threat. Masking is an effective countermeasure for reducing the statistical dependence between secret data and side-channel information. However, designing masking algorithms is an error-prone process. In this paper, we propose a hybrid approach combing type inference and model-counting to verify masked arithmetic programs against side-channel attacks. The type inference allows an efficient, lightweight procedure to determine most observable variables whereas model-counting accounts for completeness. In case that the program is not perfectly masked, we also provide a method to quantify the security level of the program. We implement our methods in a tool QMVerif and evaluate it on cryptographic benchmarks. The experimental results show the effectiveness and efficiency of our approach.

cs.CR↗

Making Agents' Abilities Explicit

Alternating-time temporal logics (ATL/ATL*) represent a family of modal logics for reasoning about agents' strategic abilities in multiagent systems (MAS). The interpretations of ATL/ATL* over the semantic model Concurrent Game Structures (CGS) usually vary depending on the agents' abilities, for instance, perfect vs. imperfect information, perfect vs. imperfect recall, resulting in a variety of variants which have been studied extensively in literature. However, they are defined at the semantic level, which may limit modeling flexibilities and may give counter-intuitive interpretations. To mitigate these issues, in this work, we propose to extend CGS with agents' abilities and study the new semantics of ATL/ATL* under this model. We give PSACE/2EXPTIME model-checking algorithms for ATL/ATL* and implement them as a prototype tool. Experiment results show the practical feasibility of the approach.

cs.AI↗

Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations

The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, whose applications include symbolic execution and automated detection of cross-site scripting (XSS) vulnerabilities. A (symbolic) path is a finite sequence of assignments and assertions (i.e. without loops), and checking its feasibility amounts to determining the existence of inputs that yield a successful execution. We give two general semantic conditions which together ensure the decidability of path feasibility: (1) each assertion admits regular monadic decomposition, and (2) each assignment uses a (possibly nondeterministic) function whose inverse relation preserves regularity. We show these conditions are expressive since they are satisfied by a multitude of string operations. They also strictly subsume existing decidable string theories, and most existing benchmarks (e.g. most of Kaluza's, and all of SLOG's, Stranger's, and SLOTH's). We give a simple decision procedure and an extensible architecture of a string solver in that a user may easily incorporate his/her own string functions. We show the general fragment has a tight, but high complexity. To address this, we propose to allow only partial string functions (i.e., prohibit nondeterminism) in condition (2). When nondeterministic functions are needed, we also provide a syntactic fragment that provides a support of nondeterministic functions but can be reduced to an existing solver SLOTH. We provide an efficient implementation of our decision procedure for deterministic partial string functions in a new string solver OSTRICH. It provides built-in support for concatenation, reverse, functional transducers, and replaceall and provides a framework for extensibility to support further string functions. We demonstrate the efficacy of our new solver against other competitive solvers.

cs.FL↗

Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints

We identify difference-bound set constraints (DBS), an analogy of difference-bound arithmetic constraints for sets. DBS can express not only set constraints but also arithmetic constraints over set elements. We integrate DBS into separation logic with linearly compositional inductive predicates, obtaining a logic thereof where set data constraints of linear data structures can be specified. We show that the satisfiability of this logic is decidable. A crucial step of the decision procedure is to compute the transitive closure of DBS-definable set relations, to capture which we propose an extension of quantified set constraints with Presburger Arithmetic (RQSPA). The satisfiability of RQSPA is then shown to be decidable by harnessing advanced automata-theoretic techniques.

cs.LO↗

Parameter Synthesis Problems for one parametric clock Timed Automata

In this paper, we study the parameter synthesis problem for a class of parametric timed automata. The problem asks to construct the set of valuations of the parameters in the parametric timed automa- ton, referred to as the feasible region, under which the resulting timed automaton satisfies certain properties. We show that the parameter syn- thesis problem of parametric timed automata with only one parametric clock (unlimited concretely constrained clock) and arbitrarily many pa- rameters is solvable when all the expressions are linear expressions. And it is moreover the synthesis problem is solvable when the form of con- straints are parameter polynomial inequality not just simple constraint and parameter domain is nonnegative real number.

cs.FL↗

What Is Decidable about String Constraints with the ReplaceAll Function

Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straight-line restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string constraints with the string-replace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straight-line fragment follows an automata-theoretic approach, and is modular in the sense that the string-replace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the state-of-the-art string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straight-line fragment with string-replace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.

cs.LO↗

The packing chromatic number of the infinite square lattice is between 13 and 15

Using a SAT-solver on top of a partial previously-known solution we improve the upper bound of the packing chromatic number of the infinite square lattice from 17 to 15. We discuss the merits of SAT-solving for this kind of problem as well as compare the performance of different encodings. Further, we improve the lower bound from 12 to 13 again using a SAT-solver, demonstrating the versatility of this technology for our approach.

cs.DM↗