Searcharxiv⌕ Search

arXiv subjects

Raphaël Khoury

Publications and source records attributed to Raphaël Khoury.

6 recordsLinked to original sources

An Empirical Analysis of ReDoS Vulnerabilities and ReDoS Detection Tools

ReDoS vulnerabilities are a type of denial of service software weakness that occurs when a regex is used to validate user-supplied input. In some cases, the regex matching process can take exponential time, leading to a denial of service. In this study, we examine and compare the effectiveness of five publicly-available regex detection tools, and one regex correction tool, using three datasets. We further perform an empirical analysis of all ReDoS vulnerabilities reported to the NVD database in order to understand how they differ from non-ReDoS vulnerabilities and glean insights about this type of weakness. We find that ReDoS vulnerabilities are becoming more prevalent and are much more likely to be exploited than non-ReDoS vulnerabilities. We further find that detection tools exhibit substantial disagreement on whether or not a given regex is vulnerable.

cs.CR↗

How Secure is Code Generated by ChatGPT?

In recent years, large language models have been responsible for great advances in the field of artificial intelligence (AI). ChatGPT in particular, an AI chatbot developed and recently released by OpenAI, has taken the field to the next level. The conversational model is able not only to process human-like text, but also to translate natural language into code. However, the safety of programs generated by ChatGPT should not be overlooked. In this paper, we perform an experiment to address this issue. Specifically, we ask ChatGPT to generate a number of program and evaluate the security of the resulting source code. We further investigate whether ChatGPT can be prodded to improve the security by appropriate prompts, and discuss the ethical aspects of using AI to generate code. Results suggest that ChatGPT is aware of potential vulnerabilities, but nonetheless often generates source code that are not robust to certain attacks.

cs.CR↗

Improving Hyperconnected Logistics with Blockchains and Smart Contracts

The Physical Internet and hyperconnected logistics concepts promise an open, more efficient and environmentally friendly supply chain for goods. Blockchain and Internet of Things technologies are increasingly regarded as main enablers of improvements in this domain. We describe how blockchain and smart contracts present the potential of being applied to hyperconnected logistics by showing a concrete example of its implementation.

cs.DC↗

Event Stream Processing with Multiple Threads

Current runtime verification tools seldom make use of multi-threading to speed up the evaluation of a property on a large event trace. In this paper, we present an extension to the BeepBeep 3 event stream engine that allows the use of multiple threads during the evaluation of a query. Various parallelization strategies are presented and described on simple examples. The implementation of these strategies is then evaluated empirically on a sample of problems. Compared to the previous, single-threaded version of the BeepBeep engine, the allocation of just a few threads to specific portions of a query provides dramatic improvement in terms of running time.

cs.DC↗

An Alternating Automaton for First-Order Linear Temporal Logic--Tech Report

In this paper we give automata-based representation of LTL-FO$^+$ properties. LTL-FO$^+$ is an extension of LTL that includes first-order quantification over bounded variable, thus greatly increasing the expressivity of the language. An automata representation of this formalism allows greater ease in writing and understanding properties, as well as in performing manipulations, such as negation or emptiness checking. The automata representation of an LTL-FO$^+$ formula has finite size regardless of the domain of quantified variables, and the number of states that is linear in the size of the property.

cs.FL↗

Runtime Enforcement With Partial Control

This study carries forward the line of enquiry that seeks to characterize precisely which security policies are enforceable by runtime monitors. In this regard, Basin et al.\ recently refined the structure that helps distinguish between those actions that the monitor can potentially suppress or insert in the execution, from those that the monitor can only observe. In this paper, we generalize this model by organizing the universe of possible actions in a lattice that naturally corresponds to the levels of monitor control. We then delineate the set of properties that are enforceable under this paradigm and relate our results to previous work in the field. Finally, we explore the set of security policies that are enforceable if the monitor is given greater latitude to alter the execution of its target, which allows us to reflect on the capabilities of different types of monitors.

cs.CR↗