Showing 1–17 of 17 results for author: Farzan, A

AI-Enabled System for Efficient and Effective Cyber Incident Detection and Response in Cloud Environments

Authors: Mohammed Ashfaaq M. Farzaan, Mohamed Chahine Ghanem, Ayman El-Hajjar, Deepthi N. Ratnayake

Abstract: The escalating sophistication and volume of cyber threats in cloud environments necessitate a paradigm shift in strategies. Recognising the need for an automated and precise response to cyber threats, this research explores the application of AI and ML and proposes an AI-powered cyber incident response system for cloud environments. This system, encompassing Network Traffic Classification, Web Int… ▽ More The escalating sophistication and volume of cyber threats in cloud environments necessitate a paradigm shift in strategies. Recognising the need for an automated and precise response to cyber threats, this research explores the application of AI and ML and proposes an AI-powered cyber incident response system for cloud environments. This system, encompassing Network Traffic Classification, Web Intrusion Detection, and post-incident Malware Analysis (built as a Flask application), achieves seamless integration across platforms like Google Cloud and Microsoft Azure. The findings from this research highlight the effectiveness of the Random Forest model, achieving an accuracy of 90% for the Network Traffic Classifier and 96% for the Malware Analysis Dual Model application. Our research highlights the strengths of AI-powered cyber security. The Random Forest model excels at classifying cyber threats, offering an efficient and robust solution. Deep learning models significantly improve accuracy, and their resource demands can be managed using cloud-based TPUs and GPUs. Cloud environments themselves provide a perfect platform for hosting these AI/ML systems, while container technology ensures both efficiency and scalability. These findings demonstrate the contribution of the AI-led system in guaranteeing a robust and scalable cyber incident response solution in the cloud. △ Less

Submitted 10 April, 2024; v1 submitted 8 April, 2024; originally announced April 2024.

Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning

Authors: Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan

Abstract: We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shine… ▽ More We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning. △ Less

Submitted 28 February, 2024; originally announced February 2024.

Comments: 23 pages + 53 pages of appendix

Commutativity Simplifies Proofs of Parameterized Programs

Authors: Azadeh Farzan, Dominik Klumpp, Andreas Podelski

Abstract: Commutativity has proven to be a powerful tool in reasoning about concurrent programs. Recent work has shown that a commutativity-based reduction of a program may admit simpler proofs than the program itself. The framework of lexicographical program reductions was introduced to formalize a broad class of reductions. Approaches based on this framework, however, were limited to program models with a… ▽ More Commutativity has proven to be a powerful tool in reasoning about concurrent programs. Recent work has shown that a commutativity-based reduction of a program may admit simpler proofs than the program itself. The framework of lexicographical program reductions was introduced to formalize a broad class of reductions. Approaches based on this framework, however, were limited to program models with a fixed number of threads. In this paper, we show that it is possible to define an effective parametric family of program reductions that can be used to find simple proofs for parameterized programs, i.e., programs with an unbounded number of threads. We show that reductions are indeed useful for the simplification of proofs of parameterized programs, in a sense that can be made precise: A reduction of a parameterized program may admit a proof which uses fewer or less sophisticated ghost variables. The reduction may therefore be within reach of an automated verification technique, even when the original parameterized program is not. We introduce a notion of reductions for parameterized programs such that the reduction $\mathcal{R}$ of a parameterized program $\mathcal{P}$ is again a parameterized program (the thread template of $\mathcal{R}$ is obtained by source-to-source transformation of the thread template of $\mathcal{P}$). Consequently, existing techniques for the verification of parameterized programs can be directly applied to $\mathcal{R}$ instead of $\mathcal{P}$. We define an appropriate family of pairwise preference orders which can be used to produce different lexicographical reductions. To determine whether this theoretical foundation amounts to a usable solution in practice, we have implemented the approach, based on a recently proposed framework for parameterized program verification. The results of our preliminary experiments on a representative set of examples are encouraging. △ Less

Submitted 5 November, 2023; originally announced November 2023.

Comments: 28 pages (26 excluding references), 8 figures, 1 table; preprint of the paper that is conditionally accepted at POPL'2024

A Pragmatic Approach to Stateful Partial Order Reduction

Authors: Berk Cirisci, Constantin Enea, Azadeh Farzan, Suha Orhun Mutluergil

Abstract: Partial order reduction (POR) is a classic technique for dealing with the state explosion problem in model checking of concurrent programs. Theoretical optimality, i.e., avoiding enumerating equivalent interleavings, does not necessarily guarantee optimal overall performance of the model checking algorithm. The computational overhead required to guarantee optimality may by far cancel out any benef… ▽ More Partial order reduction (POR) is a classic technique for dealing with the state explosion problem in model checking of concurrent programs. Theoretical optimality, i.e., avoiding enumerating equivalent interleavings, does not necessarily guarantee optimal overall performance of the model checking algorithm. The computational overhead required to guarantee optimality may by far cancel out any benefits that an algorithm may have from exploring a smaller state space of interleavings. With a focus on overall performance, we propose new algorithms for stateful POR based on the recently proposed source sets, which are less precise but more efficient than the state of the art in practice. We evaluate efficiency using an implementation that extends Java Pathfinder in the context of verifying concurrent data structures. △ Less

Submitted 21 November, 2022; originally announced November 2022.

Proving Hypersafety Compositionally

Authors: Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer

Abstract: Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between th… ▽ More Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the $n$ related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples. △ Less

Submitted 27 October, 2022; v1 submitted 15 September, 2022; originally announced September 2022.

Comments: 44 pages. Extended version of the OOPSLA'22 paper with the same title. Includes full proofs and case studies in appendix. v2 fixes typos in a derivation

ACM Class: D.2.4; F.3.1

Journal ref: Proc. ACM Program. Lang. 6, OOPSLA2, Article 135 (October 2022), 26 pages (2022)

Coarser Equivalences for Causal Concurrency

Authors: Azadeh Farzan, Umang Mathur

Abstract: Trace theory is a principled framework for defining equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by individual program threads. Its simplicity, elegance, and algorithmic efficiency makes it useful in many different contexts including program verification and testing. We study relaxations of trace equivalence with the goal of… ▽ More Trace theory is a principled framework for defining equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by individual program threads. Its simplicity, elegance, and algorithmic efficiency makes it useful in many different contexts including program verification and testing. We study relaxations of trace equivalence with the goal of maintaining its algorithmic advantages. We first prove that the largest appropriate relaxation of trace equivalence, an equivalence relation that preserves the order of steps taken by each thread and what write operation each read operation observes, does not yield efficient algorithms. We prove a linear space lower bound for the problem of checking, in a streaming setting, if two arbitrary steps of a concurrent program run are causally concurrent (i.e. they can be reordered in an equivalent run) or causally ordered (i.e. they always appear in the same order in all equivalent runs). The same problem can be decided in constant space for trace equivalence. Next, we propose a new commutativity-based notion of equivalence called grain equivalence that is strictly more relaxed than trace equivalence, and yet yields a constant space algorithm for the same problem. This notion of equivalence uses commutativity of grains, which are sequences of atomic steps, in addition to the standard commutativity from trace theory. We study the two distinct cases when the grains are contiguous subwords of the input program run and when they are not, formulate the precise definition of causal concurrency in each case, and show that they can be decided in constant space, despite being strict relaxations of the notion of causal concurrency based on trace equivalence. △ Less

Submitted 25 October, 2023; v1 submitted 25 August, 2022; originally announced August 2022.

ACM Class: F.3.1; D.3.1

Reductions for Safety Proofs (Extended Version)

Authors: Azadeh Farzan, Anthony Vandikas

Abstract: Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic classes of reductions. We introduce two classes of sound program reductions, study their theoretical properties, show how they can be effectively used in algorith… ▽ More Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic classes of reductions. We introduce two classes of sound program reductions, study their theoretical properties, show how they can be effectively used in algorithmic verification, and demonstrate that they are very effective in producing proofs of a diverse class of programs without targeting specific syntactic properties of these programs. The most novel contribution of this paper is the introduction of the concept of context in the definition of program reductions. We demonstrate how commutativity of program steps in some program contexts can be used to define a generic class of sound reductions which can be used to automatically produce proofs for programs whose complete Floyd-Hoare style proofs are theoretically beyond the reach of automated verification technology of today. △ Less

Submitted 31 October, 2019; originally announced October 2019.

Reductions for Automated Hypersafety Verification

Authors: Azadeh Farzan, Anthony Vandikas

Abstract: We propose an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. The key observation is that constructing a proof for a small representative set of the runs of the product program (i.e. the product of the several copies of the program by itself), called a reduction, is sufficient to formally prove the h… ▽ More We propose an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. The key observation is that constructing a proof for a small representative set of the runs of the product program (i.e. the product of the several copies of the program by itself), called a reduction, is sufficient to formally prove the hypersafety property about the program. We propose an algorithm based on a counterexample-guided refinement loop that simultaneously searches for a reduction and a proof of the correctness for the reduction. We demonstrate that our tool Weaver is very effective in verifying a diverse array of hypersafety properties for a diverse class of input programs. △ Less

Submitted 22 May, 2019; originally announced May 2019.

Modular Synthesis of Divide-and-Conquer Parallelism for Nested Loops (Extended Version)

Authors: Azadeh Farzan, Victor Nicolet

Abstract: We propose a methodology for automatic generation of divide-and-conquer parallel implementations of sequential nested loops. We focus on a class of loops that traverse read-only multidimensional collections (lists or arrays) and compute a function over these collections. Our approach is modular, in that, the inner loop nest is abstracted away to produce a simpler loop nest for parallelization. The… ▽ More We propose a methodology for automatic generation of divide-and-conquer parallel implementations of sequential nested loops. We focus on a class of loops that traverse read-only multidimensional collections (lists or arrays) and compute a function over these collections. Our approach is modular, in that, the inner loop nest is abstracted away to produce a simpler loop nest for parallelization. Then, the summarized version of the loop nest is parallelized. The main challenge addressed by this paper is that to perform the code transformations necessary in each step, the loop nest may have to be augmented (automatically) with extra computation to make possible the abstraction and/or the parallelization tasks. We present theoretical results to justify the correctness of our modular approach, and algorithmic solutions for automation. Experimental results demonstrate that our approach can parallelize highly non-trivial loop nests efficiently. △ Less

Submitted 1 April, 2019; originally announced April 2019.

Comments: This is the extended version of PLDI 2019 paper by the same authors which includes the proofs of theorems and additional details

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

Authors: Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner, Julian Sutherland

Abstract: We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is w… ▽ More We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients which use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants, and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies. △ Less

Submitted 29 November, 2021; v1 submitted 17 January, 2019; originally announced January 2019.

Comments: 84 pages, 131 pages including appendix

MSC Class: F.3.1; D.2.4 ACM Class: F.3.1; D.2.4

Journal ref: ACM Transactions on Programming Languages and Systems, Volume 43 Issue 4 (2021) pp 1-134

Automated Synthesis of Divide and Conquer Parallelism

Authors: Azadeh Farzan, Victor Nicolet

Abstract: This paper focuses on automated synthesis of divide-and-conquer parallelism, which is a common parallel programming skeleton supported by many cross-platform multithreaded libraries. The challenges of producing (manually or automatically) a correct divide-and-conquer parallel program from a given sequential code are two-fold: (1) assuming that individual worker threads execute a code identical to… ▽ More This paper focuses on automated synthesis of divide-and-conquer parallelism, which is a common parallel programming skeleton supported by many cross-platform multithreaded libraries. The challenges of producing (manually or automatically) a correct divide-and-conquer parallel program from a given sequential code are two-fold: (1) assuming that individual worker threads execute a code identical to the sequential code, the programmer has to provide the extra code for dividing the tasks and combining the computation results, and (2) sometimes, the sequential code may not be usable as is, and may need to be modified by the programmer. We address both challenges in this paper. We present an automated synthesis technique for the case where no modifications to the sequential code are required, and we propose an algorithm for modifying the sequential code to make it suitable for parallelization when some modification is necessary. The paper presents theoretical results for when this {\em modification} is efficiently possible, and experimental evaluation of the technique and the quality of the produced parallel programs. △ Less

Submitted 28 January, 2017; originally announced January 2017.

Proving Liveness of Parameterized Programs

Authors: Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Abstract: Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument… ▽ More Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold regardless of the number of threads that are active in the program. △ Less

Submitted 8 May, 2016; originally announced May 2016.

Compositional Invariant Generation via Linear Recurrence Analysis

Authors: Azadeh Farzan, Zachary Kincaid

Abstract: This paper presents a new method for automatically generating numerical invariants for imperative programs. Given a program, our procedure computes a binary input/output relation on program states which over-approximates the behaviour of the program. It is compositional in the sense that it operates by decomposing the program into parts, computing an abstract meaning of each part, and then composi… ▽ More This paper presents a new method for automatically generating numerical invariants for imperative programs. Given a program, our procedure computes a binary input/output relation on program states which over-approximates the behaviour of the program. It is compositional in the sense that it operates by decomposing the program into parts, computing an abstract meaning of each part, and then composing the meanings. Our method for approximating loop behaviour is based on first approximating the meaning of the loop body, extracting recurrence relations from that approximation, and then using the closed forms to approximate the loop. Our experiments demonstrate that on verification tasks, our method is competitive with leading invariant generation and verification tools. △ Less

Submitted 31 January, 2015; originally announced February 2015.

Algorithms in the Ultra-Wide Word Model

Authors: Arash Farzan, Alejandro López-Ortiz, Patrick K. Nicholson, Alejandro Salinger

Abstract: The effective use of parallel computing resources to speed up algorithms in current multi-core parallel architectures remains a difficult challenge, with ease of programming playing a key role in the eventual success of various parallel architectures. In this paper we consider an alternative view of parallelism in the form of an ultra-wide word processor. We introduce the Ultra-Wide Word architect… ▽ More The effective use of parallel computing resources to speed up algorithms in current multi-core parallel architectures remains a difficult challenge, with ease of programming playing a key role in the eventual success of various parallel architectures. In this paper we consider an alternative view of parallelism in the form of an ultra-wide word processor. We introduce the Ultra-Wide Word architecture and model, an extension of the word-RAM model that allows for constant time operations on thousands of bits in parallel. Word parallelism as exploited by the word-RAM model does not suffer from the more difficult aspects of parallel programming, namely synchronization and concurrency. For the standard word-RAM algorithms, the speedups obtained are moderate, as they are limited by the word size. We argue that a large class of word-RAM algorithms can be implemented in the Ultra-Wide Word model, obtaining speedups comparable to multi-threaded computations while kee** the simplicity of programming of the sequential RAM model. We show that this is the case by describing implementations of Ultra-Wide Word algorithms for dynamic programming and string searching. In addition, we show that the Ultra-Wide Word model can be used to implement a nonstandard memory architecture, which enables the sidestep** of lower bounds of important data structure problems such as priority queues and dynamic prefix sums. While similar ideas about operating on large words have been mentioned before in the context of multimedia processors [Thorup 2003], it is only recently that an architecture like the one we propose has become feasible and that details can be worked out. △ Less

Submitted 7 December, 2014; v1 submitted 26 November, 2014; originally announced November 2014.

Comments: 28 pages, 5 figures; minor changes

ACM Class: F.1.1; F.1.2; F.2.2

An Algebraic Framework for Compositional Program Analysis

Authors: Azadeh Farzan, Zachary Kincaid

Abstract: The purpose of a program analysis is to compute an abstract meaning for a program which approximates its dynamic behaviour. A compositional program analysis accomplishes this task with a divide-and-conquer strategy: the meaning of a program is computed by dividing it into sub-programs, computing their meaning, and then combining the results. Compositional program analyses are desirable because the… ▽ More The purpose of a program analysis is to compute an abstract meaning for a program which approximates its dynamic behaviour. A compositional program analysis accomplishes this task with a divide-and-conquer strategy: the meaning of a program is computed by dividing it into sub-programs, computing their meaning, and then combining the results. Compositional program analyses are desirable because they can yield scalable (and easily parallelizable) program analyses. This paper presents algebraic framework for designing, implementing, and proving the correctness of compositional program analyses. A program analysis in our framework defined by an algebraic structure equipped with sequencing, choice, and iteration operations. From the analysis design perspective, a particularly interesting consequence of this is that the meaning of a loop is computed by applying the iteration operator to the loop body. This style of compositional loop analysis can yield interesting ways of computing loop invariants that cannot be defined iteratively. We identify a class of algorithms, the so-called path-expression algorithms [Tarjan1981,Scholz2007], which can be used to efficiently implement analyses in our framework. Lastly, we develop a theory for proving the correctness of an analysis by establishing an approximation relationship between an algebra defining a concrete semantics and an algebra defining an analysis. △ Less

Submitted 13 October, 2013; originally announced October 2013.

Comments: 15 pages

Succinct Indices for Range Queries with applications to Orthogonal Range Maxima

Authors: Arash Farzan, J. Ian Munro, Rajeev Raman

Abstract: We consider the problem of preprocessing $N$ points in 2D, each endowed with a priority, to answer the following queries: given a axis-parallel rectangle, determine the point with the largest priority in the rectangle. Using the ideas of the \emph{effective entropy} of range maxima queries and \emph{succinct indices} for range maxima queries, we obtain a structure that uses O(N) words and answers… ▽ More We consider the problem of preprocessing $N$ points in 2D, each endowed with a priority, to answer the following queries: given a axis-parallel rectangle, determine the point with the largest priority in the rectangle. Using the ideas of the \emph{effective entropy} of range maxima queries and \emph{succinct indices} for range maxima queries, we obtain a structure that uses O(N) words and answers the above query in $O(\log N \log \log N)$ time. This is a direct improvement of Chazelle's result from FOCS 1985 for this problem -- Chazelle required $O(N/ε)$ words to answer queries in $O((\log N)^{1+ε})$ time for any constant $ε> 0$. △ Less

Submitted 21 April, 2012; originally announced April 2012.

Comments: To appear in ICALP 2012

Report number: Leicester CS-TR-12-001

Priority Queues with Multiple Time Fingers

Authors: Amr Elmasry, Arash Farzan, John Iacono

Abstract: A priority queue is presented that supports the operations insert and find-min in worst-case constant time, and delete and delete-min on element x in worst-case O(lg(min{w_x, q_x}+2)) time, where w_x (respectively q_x) is the number of elements inserted after x (respectively before x) and are still present at the time of the deletion of x. Our priority queue then has both the working-set and the q… ▽ More A priority queue is presented that supports the operations insert and find-min in worst-case constant time, and delete and delete-min on element x in worst-case O(lg(min{w_x, q_x}+2)) time, where w_x (respectively q_x) is the number of elements inserted after x (respectively before x) and are still present at the time of the deletion of x. Our priority queue then has both the working-set and the queueish properties, and more strongly it satisfies these properties in the worst-case sense. We also define a new distribution-sensitive property---the time-finger property, which encapsulates and generalizes both the working-set and queueish properties, and present a priority queue that satisfies this property. In addition, we prove a strong implication that the working-set property is equivalent to the unified bound (which is the minimum per operation among the static finger, static optimality, and the working-set bounds). This latter result is of tremendous interest by itself as it had gone unnoticed since the introduction of such bounds by Sleater and Tarjan [JACM 1985]. Accordingly, our priority queue satisfies other distribution-sensitive properties as the static finger, static optimality, and the unified bound. △ Less

Submitted 28 September, 2010; originally announced September 2010.

Comments: 14 pages, 4 figures

ACM Class: E.1