Publications

2024

PLDI
Propel

Automated Verification of Fundamental Algebraic Laws

George Zakhour, Pascal Weisenburger, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 8 (PLDI), 2024

Abstract PDF Supp Code Website

Algebraic laws of functions in mathematics – such as commutativity, associativity, and idempotence – are often used as the basis to derive more sophisticated properties of complex mathematical structures and are heavily used in abstract computational thinking. Algebraic laws of functions in coding, however, are rarely considered. Yet, they are essential. For example, commutativity and associativity are crucial to ensure correctness of a variety of software systems in numerous domains, such as compiler optimization, big data processing, data flow processing, machine learning or distributed algorithms and data structures. Still, most programming languages lack built-in mechanisms to enforce and verify that operations adhere to such properties.
In this paper, we propose a verifier specialized on a set of fundamental algebraic laws that ensures that such laws hold in application code. The verifier can conjecture auxiliary properties and can reason about both equalities and inequalities of expressions, which is crucial to prove a given property when other competitors do not succeed. We implement these ideas in the Propel verifier. Our evaluation against five state-of-the-art verifiers on a total of 142 instances of algebraic properties shows that Propel is able to automatically deduce algebraic properties in different domains that rely on such properties for correctness, even in cases where competitors fail to verify the same properties or time out.
EDBT

Stateful Entities: Object-oriented Cloud Applications as Distributed Dataflows

Kyriakos Psarakis, Wouter Zorgdrager, Marios Fragkoulis, Guido Salvaneschi, Asterios Katsifodimos

In Proceedings of the 27th International Conference on Extending Database Technology, EDBT, 2024

Abstract PDF

Although the cloud has reached a state of robustness, the burden of using its resources falls on the shoulders of programmers who struggle to keep up with ever-growing cloud infrastructure services and abstractions. As a result, state management, scaling, operation, and failure management of scalable cloud applications, require disproportionately more effort than developing the applications’ actual business logic.
Our vision aims to raise the abstraction level for programming scalable cloud applications by compiling stateful entities – a programming model enabling imperative transactional programs authored in Python – into stateful streaming dataflows. We propose a compiler pipeline that analyzes the abstract syntax tree of stateful entities and transforms them into an intermediate representation based on stateful dataflow graphs. It then compiles that intermediate representation into different dataflow engines, leveraging their exactly-once message processing guarantees to prevent state or failure management primitives from “leaking” into the level of the programming model. Preliminary experiments with a proof of concept implementation show that despite program transformation and translation to dataflows, stateful entities can perform at sub-100ms latency even for transactional workloads.
LNCS
ScalaLoci

Bridging Between Active Objects: Multitier Programming for Distributed, Concurrent Systems

Guido Salvaneschi, Pascal Weisenburger

In Active Object Languages: Current Research Trends, Lecture Notes in Computer Science, 2024

Abstract PDF

Programming distributed and concurrent systems is notoriously hard. Active objects, which encapsulate operations, state and control flow, have been investigated by researchers to alleviate this issue. In a distributed system, message exchange among active objects or actors often coincides with network boundaries, and determines a major modularization direction for the application. Yet, certain application functionalities naturally crosscut such modularization direction. For those, structuring the application architecture around network boundaries is purely accidental and does not help reasoning about programs.
Recently, multitier programming has been proposed as a programming paradigm that enables code that belongs to different peers to be developed together, in the same compilation unit. The compiler then splits the code and generates the required deployment components.
In this work we explore the relation between multitier programming and active objects. Multitier programming can be considered a programming paradigm based on active objects with a focus on application domains where functionalities span multiple active objects, and allows such functionalities to be encapsulated into a single object. The multitier approach keeps the asynchronous model of active objects and actors but provides a holistic view of distributed components and their interactions. Multitier programming addresses the use cases where separating components into different active objects or actors hinders encapsulation and modularization across functional boundaries. In such use cases, multitier programming can increase the level of abstraction, improve software design, simplify code maintenance, aid program comprehension and enable formal reasoning. A number of features of active objects are directly visible to programmers also in the multitier programming, resulting in an interesting combination of language abstractions available to developers.
TSE
ProTI

Automated Infrastructure as Code Program Testing

Daniel Sokolowski, David Spielmann, Guido Salvaneschi

IEEE Transactions on Software Engineering, 2024

PDF Supp Code Website
ICSE Companion
ProTI

Unleashing the Giants: Enabling Advanced Testing for Infrastructure as Code

Daniel Sokolowski, David Spielmann, Guido Salvaneschi

In Companion Proceedings of the 46th International Conference on Software Engineering, ICSE Companion, 2024

PDF
MSR

The PIPr Dataset of Public Infrastructure as Code Programs

Daniel Sokolowski, David Spielmann, Guido Salvaneschi

In Proceedings of the IEEE/ACM 21st International Conference on Mining Software Repositories, MSR, 2024

PDF

2023

OOPSLA
ScalaLoci

Type-Safe Dynamic Placement with First-Class Placed Values

George Zakhour, Pascal Weisenburger, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 2023

Abstract PDF Supp Code Website

Several distributed programming language solutions have been proposed to reason about the placement of data, computations, and peers interaction. Such solutions include, among the others, multitier programming, choreographic programming and various approaches based on behavioral types. These methods statically ensure safety properties thanks to a complete knowledge about placement of data and computation at compile time. In distributed systems, however, dynamic placement of computation and data is crucial to enable performance optimizations, e.g., driven by data locality or in presence of a number of other constraints such as security and compliance regarding data storage location. Unfortunately, in existing programming languages, dynamic placement conflicts with static reasoning about distributed programs: the flexibility required by dynamic placement hinders statically tracking the location of data and computation.
In this paper we present Dyno, a programming language that enables static reasoning about dynamic placement. Dyno features a type system where values are explicitly placed, but in contrast to existing approaches, placed values are also first class, ensuring that they can be passed around and referred to from other locations. Building on top of this mechanism, we provide a novel interpretation of dynamic placement as unions of placement types. We formalize type soundness, placement correctness (as part of type soundness) and architecture conformance. In case studies and benchmarks, our evaluation shows that Dyno enables static reasoning about programs even in presence of dynamic placement, ensuring type safety and placement correctness of programs at negligible performance cost. We reimplement an Android app with 7K LOC in Dyno, find a bug in the existing implementation, and show that the app’s approach is representative of a common way to implement dynamic placement found in over 100 apps in a large open-source app store.
TOPLAS

Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications

David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, Mira Mezini

ACM Transactions on Programming Languages and Systems 45 (3), 2023

Abstract PDF

Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs – in different programming languages – communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses.
In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit and pairs of send and receive actions that “belong together” are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.
PLDI
Propel

Type-Checking CRDT Convergence

George Zakhour, Pascal Weisenburger, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 7 (PLDI), 2023

Abstract PDF Supp Code Website

Conflict-free Replicated Data Types (CRDTs) are a recent approach for keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. For correct operation, CRDTs rely on a merge function that is commutative, associative and idempotent. Ensuring that such algebraic properties are satisfied by implementations, however, is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of a model, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations.
In this paper, we present Propel, a programming language with a type system that captures the algebraic properties required by a correct CRDT implementation. The Propel type system deduces such properties by case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction for free. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties. We provide an implementation of Propel as a Scala embedding, we implement several CRDTs, verify them with Propel and compare the verification process with four state-of-the-art verification tools. Our evaluation shows that Propel is able to automatically deduce the properties that are relevant for common CRDT implementations found in open-source libraries even in cases in which competitors timeout.
JSS

The Uphill Journey of FaaS in the Open-Source Community

Nafise Eskandani, Guido Salvaneschi

Journal of Systems and Software 198, 2023

Abstract PDF

Since its introduction in 2014 by Amazon, the Function as a Service (FaaS) model of serverless computing has set the expectation to fulfill the promise of on-demand, pay-as-you-go, infrastructure-independent processing, originally formulated by cloud computing. Yet, serverless applications are fundamentally different than traditional service-oriented software in that they pose specific performance (e.g., cold start), design (e.g., stateless), and development challenges (e.g., debugging). A growing number of cloud solutions have been continuously attempting to address each of these challenges as a result of the increasing popularity of FaaS. Yet, the characteristics of this model have been poorly understood; therefore, the challenges are poorly tackled. In this paper, we assess the state of FaaS in open-source community with a study on almost 2K real-world serverless applications. Our results show a jeopardized ecosystem, where, despite the hype of serverless solutions in the last years, a number of challenges remain untackled, especially concerning component reuse, support for software development, and flexibility among different platforms – resulting in arguably slow adoption of the FaaS model. We believe that addressing the issues discussed in this paper may help researchers shaping the next generation of cloud computing models.
FIST
ProTI

Towards Reliable Infrastructure as Code

Daniel Sokolowski, Guido Salvaneschi

In Companion Proceedings of 2023 IEEE 20th International Conference on Software Architecture, ICSA Companion, 2023

Abstract PDF

Modern Infrastructure as Code (IaC) programs are increasingly complex and much closer to traditional software than to simple configuration scripts. Their reliability is crucial because their failure prevents the deployment of applications, and incorrect behavior can introduce malfunction and severe security issues. Yet, software engineering tools to develop reliable programs, such as testing and verification, are barely used in IaC. In fact, we observed that developers mainly rely on integration testing, a slow and expensive practice that can increase confidence in end-to-end functionality but is infeasible to systematically test IaC programs in various configurations—which is required to ensure robustness. On the other hand, fast testing techniques, such as unit testing, are cumbersome with IaC programs because, today, they require significant coding overhead while only providing limited confidence.
To solve this issue, we envision the automated testing tool ProTI, reducing the manual overhead and boosting confidence in the test results. ProTI embraces modern unit testing techniques to test IaC programs in many different configurations. Out of the box, ProTI is a fuzzer for Pulumi TypeScript IaC programs, randomly testing the program in many different configurations for termination, configuration correctness, and existing policy compliance. Then developers can add specifications to their program to guide random-based value generation, test additional properties, and add further mocking, making ProTI a property-based testing tool. Lastly, we aim at automatically verifying IaC-specific properties, e.g., access paths between resources.
IEEE Software
µs

Decentralizing Infrastructure as Code

Daniel Sokolowski, Pascal Weisenburger, Guido Salvaneschi

IEEE Software 40 (1), 2023

Abstract PDF

Infrastructure as Code (IaC) automates deployments for single teams, falling short of decentralized deployments across groups. We need mature IaC solutions that embrace and consolidate software engineering principles to enable testing and automation advances for decentralized organizations.
CONFLANG
ProTI

Creed for Speed: Comprehensive Infrastructure as Code Testing

Daniel Sokolowski, David Spielmann, Guido Salvaneschi

Presentation at the CONFLANG 2023 workshop, 2023

Abstract PDF

With Programming Languages Infrastructure as Code (PL-IaC), developers implement imperative IaC programs in one of many general-purpose programming languages, e.g., TypeScript, Python, or Go, to declaratively describe deployments. Using these languages provides access to quality assurance techniques and tools developed for traditional software; however, programmers routinely rely on prohibitively slow integration testing – if they test at all. As a result, even simple bugs are found late, tremendously slowing down the development process.
To improve the velocity of PL-IaC development, we propose ProTI, an automated unit testing approach that quickly tests PL-IaC programs in many different configurations. ProTI mocks all cloud resources, replacing them with pluggable oracles that validate all resources configurations and a generator for realistic test inputs. We implemented ProTI for Pulumi TypeScript with simple generator and oracle plugins. Our experience of testing with ProTI encourages the exploration of more sophisticated oracles and generators, leading to the early detection of more bugs. ProTI enables programmers to rapidly prototype, explore, and plug in new oracles and generators for efficient PL-IaC program testing.
SPLASH Companion
ProTI

Extensible Testing for Infrastructure as Code

David Spielmann, Daniel Sokolowski, Guido Salvaneschi

In Companion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH Companion, 2023

Abstract PDF

Developers automate deployments with Programming Languages Infrastructure as Code (PL-IaC) by implementing IaC programs in popular languages like TypeScript and Python. Yet, systematic testing—well established for high-velocity software development—is rarely applied to IaC programs because IaC testing techniques are either slow or require extensive development effort. To solve this dilemma, we develop ProTI, a novel IaC unit testing approach, and implement it for Pulumi TypeScript. Our preliminary experiments with simple type-based test case generators and oracles show that ProTI can find bugs reliably in a short time, often without writing any additional testing code. ProTI’s extensible plugin architecture allows combining, adopting, and experimenting with new approaches, opening the discussion about novel generators and oracles for efficient IaC testing.
SPLASH Companion
ConSysT

Safe Combination of Data-Centric and Operation-Centric Consistency

Mirko Köhler, Guido Salvaneschi

In Companion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH Companion, 2023

Abstract PDF

Programming distributed systems requires maintaining consistency among data replicas. In recent years, various frameworks have proposed language-level abstractions for this, falling into two fundamental approaches: data-centric and operation-centric solutions. The former allow developers to explicitly assign consistency levels to data, the latter enable attaching consistency constraints to operations. In practice, developers may benefit from both in the same application: data-centric consistency harmonizes well with object-oriented programming, yet one may need the flexibility to access the same data with a different consistency level depending on the operation. Currently, there is no solution that integrates both: it is a conceptual challenge to unify these two models and design a type system capable of ensuring their correct interaction.
We present ConOpY, a programming language that integrates both data-centric and operation-centric consistency into the same design. The ConOpY type system guarantees the proper usage of consistency levels, preventing consistency violations resulting from an improper mix of consistency models. ConOpY is implemented as a Java extension based on annotations.

2022

ESEC/FSE DS
µs

Infrastructure as Code for Dynamic Deployments

Daniel Sokolowski

In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE, 2022

Abstract PDF

Modern DevOps organizations require a high degree of automation to achieve software stability at frequent changes. Further, there is a need for flexible, timely reconfiguration of the infrastructure, e.g., to use pay-per-use infrastructure efficiently based on application load. Infrastructure as Code (IaC) is the DevOps tool to automate infrastructure. However, modern static IaC solutions only support infrastructures that are deployed and do not change afterward. To implement infrastructures that change dynamically over time, static IaC programs have to be (updated and) re-run, e.g., in a CI/CD pipeline, or configure an external orchestrator that implements the dynamic behavior, e.g., an autoscaler or Kubernetes operator. Both do not capture the dynamic behavior in the IaC program and prevent analyzing and testing the infrastructure configuration jointly with its dynamic behavior.
To fill this gap, we envision dynamic IaC, which augments static IaC with the ability to define dynamic behavior within the IaC program. In contrast to static IaC programs, dynamic IaC programs run continuously. They re-evaluate program parts that depend on external signals when these change and automatically adjust the infrastructure accordingly. We implement DIaC as the first dynamic IaC solution and demonstrate it in two realistic use cases of broader relevance. With dynamic IaC, ensuring the program’s correctness is even harder than for static IaC because programs may define many target configurations in contrast to only a few. However, for this reason, it is also more critical. To solve this issue, we propose automated, specialized property-based testing for IaC programs and implement it in ProTI.
ECOOP

Functional Programming for Distributed Systems with XC

Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Guido Salvaneschi, Mirko Viroli

In Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2022

Abstract PDF

Programming distributed systems is notoriously hard due to – among the others – concurrency, asynchronous execution, message loss, and device failures. Homogeneous distributed systems consist of similar devices that communicate to neighbors and execute the same program: they include wireless sensor networks, network hardware and robot swarms. For the homogeneous case, we investigate an experimental language design that aims to push the abstraction boundaries farther, compared to existing approaches.
In this paper, we introduce the design of XC, a programming language to develop homogeneous distributed systems. In XC, developers define the single program that every device executes and the overall behavior is achieved collectively, in an emergent way. The programming framework transparently takes care of concurrency, asynchronous execution, message loss, and device failures. We propose a minimalistic design, which features a single declarative primitive for communication, state management and connection management. A mechanism called alignment enables developers to abstract over asynchronous execution while still retaining composability. We define syntax and operational semantics of a core calculus, prove a number of properties of the calculus, including type soundness. XC comes with two DSL implementations: a DSL in Scala and one in C++. An evaluation based on smart-city monitoring demonstrates XC in a realistic application.
ECOOP

Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract)

David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, Mira Mezini

In Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2022

Abstract PDF Supp

Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs – in different programming languages – communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses.
In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit and pairs of send and receive actions that “belong together” are encapsulated into a single direct–style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.
ICSE

Change Is the Only Constant: Dynamic Updates for Workflows

Daniel Sokolowski, Pascal Weisenburger, Guido Salvaneschi

In Proceedings of the 44th International Conference on Software Engineering, ICSE, 2022

Abstract PDF Supp

Software systems must be updated regularly to address changing requirements and urgent issues like security-related bugs. Traditionally, updates are performed by shutting down the system to replace certain components. In modern software organizations, updates are increasingly frequent—up to multiple times per day—hence, shutting down the entire system is unacceptable. Safe dynamic software updating (DSU) enables component updates while the system is running by determining when the update can occur without causing errors. Safe DSU is crucial, especially for long-running or frequently executed asynchronous transactions (workflows), e.g., user-interactive sessions and order fulfillment processes. Unfortunately, previous research is limited to synchronous transaction models and does not address this case.
In this work, we propose a unified model for safe DSU in workflows. We discuss how state-of-the-art DSU solutions fit into this model and show that they incur significant overhead. To improve the performance, we introduce Essential Safety, a novel safe DSU approach that leverages the notion of non-essential changes, i.e., semantics preserving updates. In 106 realistic collaborative BPMN workflows, Essential Safety reduces the delay of workflow completions, on average, by 47.8% compared to the state of the art. We show that the distinction of essential and non-essential changes plays a crucial role in this reduction and that, as suggested in literature, non-essential changes are frequent: at least 60% and often more than 90% of systems’ updates in eight monorepos we analyze.

2021

JCSS

TCEP: Transitions in Operator Placement to Adapt to Dynamic Network Environments

Manisha Luthra, Boris Koldehofe, Niels Danger, Pascal Weisenburger, Guido Salvaneschi, Ioannis Stavrakakis

Journal of Computer and System Sciences 122, 2021

Abstract PDF

Distributed Complex Event Processing (DCEP) is a commonly used paradigm to detect and act on situational changes of many applications, including the Internet of Things (IoT). DCEP achieves this using a simple specification of analytical tasks on data streams called operators and their distributed execution on a set of infrastructure. The adaptivity of DCEP to the dynamics of IoT applications is essential and very challenging in the face of changing demands concerning Quality of Service. In our previous work, we addressed this issue by enabling transitions, which allow for the adaptive use of operator placement mechanisms. In this article, we extend the transition methodology by optimizing the costs of transition and analyzing the behavior using multiple operator placement mechanisms. Furthermore, we provide an extensive evaluation on the costs of transition imposed by operator migrations and learning, as it can inflict overhead on the performance if operated uncoordinatedly.
PAVeTrust
J_E

Towards Democratizing Secure Enclave Programming

Aditya Oak, Amir M. Ahmadian, Musard Balliu, Guido Salvaneschi

In Program Analysis and Verification on Trusted Platforms, PAVeTrust, 2021

Abstract PDF

Secure enclaves, like Intel SGX, provide a means to process data securely on third-party cloud infrastructure with little or no performance overhead. Developing software that takes advantage of a secure enclave requires, however, to explicitly deal with a number of low-level details such as dedicated IO, custom syscalls, and stringent memory constraints, requiring the expertise needed for system programming, rather than applications. We discuss our recent research that provides a developer-friendly approach to enclave programming—our Java language extension JE. Finally, we outline our vision of a programming framework that brings secure enclave programming at the fingertips of application developers.
SecDev
J_E

Enclave-Based Secure Programming with JE

Aditya Oak, Amir M. Ahmadian, Musard Balliu, Guido Salvaneschi

In Proceedings of the 2021 IEEE Secure Development Conference, SecDev, 2021

Abstract PDF

Over the past few years, major hardware vendors have started offering processors that support Trusted Execution Environments (TEEs) allowing confidential computations over sensitive data on untrusted hosts. Unfortunately, developing applications that use TEEs remains challenging. Current solutions require to use low-level languages (e.g., C/C++) to handle the TEE management process manually – a complex and error-prone task. Worse, the separation of the application into components that run inside and outside the TEE may lead to information leaks. In summary, TEEs are a powerful means to design secure applications, but there is still a long way to building secure software with TEEs alone.
In this work, we present , a programming model for developing TEE-enabled applications where developers only need to annotate Java programs to define application-level security policies and run them securely inside enclaves.
ESEC/FSE
µs

Automating Serverless Deployments for DevOps Organizations

Daniel Sokolowski, Pascal Weisenburger, Guido Salvaneschi

In Proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE, 2021

Abstract PDF Supp Code

DevOps unifies software development and operations in cross-functional teams to improve software delivery and operations (SDO) performance. Ideally, cross-functional DevOps teams independently deploy their services, but the correct operation of a service often demands other services, requiring coordination to ensure the correct deployment order. This issue is currently solved either with a central deployment or manual out-of-band communication across teams, e.g., via phone, chat, or email. Unfortunately, both contradict the independence of teams, hindering SDO performance – the reason why DevOps is adopted in the first place.
In this work, we conduct a study on 73 IT professionals, showing that, in practice, they resort to manual coordination for correct deployments even if they expect better SDO performance with fully automated approaches. To address this issue, we propose μs ([mju:z] “muse”), a novel IaC system automating deployment coordination in a fully decentralized fashion, still retaining compatibility with DevOps practice – in contrast to today’s solutions. We implement µs, demonstrate that it effectively enables automated coordination, introduces negligible definition overhead, has no performance overhead, and is broadly applicable, as shown by the migration of 64 third-party IaC projects.
ESEC/FSE DS
µs

Deployment Coordination for Cross-Functional DevOps Teams

Daniel Sokolowski

In Proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE, 2021

Abstract PDF

Software stability and reliability are the core concerns of DevOps. They are improved by tightening the collaboration between developers and operators in cross-functional teams on the one hand and by automating operations through continuous integration (CI) and infrastructure as code (IaC) on the other hand. Ideally, teams in DevOps are fully independent. Still, their applications often depend on each other in practice, requiring them to coordinate their deployment through centralization or manual coordination.
With this work, we propose and implement the novel IaC solution µs ([mju:z] “muse”), which automates deployment coordination in a decentralized fashion. µs is the first approach that is compatible with the DevOps goals as it enables truly independent operations of the DevOps teams. We define our research problem through a questionnaire survey with IT professionals and evaluate the solution by comparing it to other modern IaC approaches, assessing its performance, and applying it to existing IaC programs.
AISTA

Impact of Programming Languages on Machine Learning Bugs

Sebastian Sztwiertnia, Maximilian Grübel, Amine Chouchane, Daniel Sokolowski, Krishna Narasimhan, Mira Mezini

In Proceedings of the 1st ACM International Workshop on AI and Software Testing/Analysis, AISTA, 2021

Abstract PDF

Machine learning (ML) is on the rise to be ubiquitous in modern software. Still, its use is challenging for software developers. So far, research has focused on the ML libraries to find and mitigate these challenges. However, there is initial evidence that programming languages also add to the challenges, identifiable in different distributions of bugs in ML programs. To fill this research gap, we propose the first empirical study on the impact of programming languages on bugs in ML programs. We plan to analyze software from GitHub and related discussions in GitHub issues and Stack Overflow for bug distributions in ML programs, aiming to identify correlations with the chosen programming language, its features and the application domain. This study’s results enable better-targeted use of available programming language technology in ML programs, preventing bugs, reducing errors and speeding up development.
ECOOP
ScalaLoci

Multiparty Languages: The Choreographic and Multitier Cases

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, Pascal Weisenburger

In Proceedings of the 35th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2021

Abstract PDF

Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings—respectively process calculi and lambda calculus—the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long.
In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.
CSF
J_E

Language Support for Secure Software Development with Enclaves

Aditya Oak, Amir M. Ahmadian, Musard Balliu, Guido Salvaneschi

In Proceedings of the 34th IEEE Computer Security Foundations Symposium, CSF, 2021

Abstract PDF

Confidential computing is a promising technology for securing code and data-in-use on untrusted host machines, e.g., the cloud. Many hardware vendors offer different implementations of Trusted Execution Environments (TEEs). A TEE is a hardware protected execution environment that allows performing confidential computations over sensitive data on untrusted hosts. Despite the appeal of achieving strong security guarantees against low-level attackers, two challenges hinder the adoption of TEEs. First, developing software in high-level managed languages, e.g., Java or Scala, taking advantage of existing TEEs is complex and error-prone. Second, partitioning an application into components that run inside and outside a TEE may break application-level security policies, resulting in an insecure application when facing a realistic attacker.
In this work, we study both these challenges. We present J_E, a programming model that seamlessly integrates a TEE, abstracting away low-level programming details such as initialization and loading of data into the TEE. J_E only requires developers to add annotations to their programs to enable the execution within the TEE. Drawing on information flow control, we develop a security type system that checks confidentiality and integrity policies against realistic attackers with full control over the code running outside the TEE. We formalize the security type system for the J_E core and prove it sound for a semantic characterization of security. We implement J_E and the security type system, enable Java programs to run on Intel SGX with strong security guarantees. We evaluate our approach on use cases from the literature, including a battleship game, a secure event processing system, and a popular processing framework for big data, showing that we correctly handle complex cases of partitioning, information flow, declassification, and trust.
MSR

The Wonderless Dataset for Serverless Computing

Nafise Eskandani, Guido Salvaneschi

In Proceedings of the IEEE/ACM 18th International Conference on Mining Software Repositories, MSR, 2021

Abstract PDF

Function as a Service (FaaS) has grown in popularity in recent years, with an increasing number of applications following the Serverless computing model. Serverless computing supports out of the box autoscaling in a pay-as-you-go manner, letting developers focus on the application logic rather than worrying about resource management. With the increasing adoption of the this model, researchers have started studying a wide variety of aspects of Serverless computing, including communication, security, performance, and cost optimization. Yet, we still know very little of how Serverless computing is used in practice.
In this paper, we introduce Wonderless, a novel dataset of open-source Serverless applications. Wonderless consists of 1,877 real-world Serverless applications extracted from GitHub, and it can be used as a data source for further research in the Serverless ecosystem, such as performance evaluation and software mining. To the best of our knowledge, Wonderless is currently the most diverse and largest dataset for research on Serverless computing.

2020

OOPSLA

Handling Bidirectional Control Flow

Yizhou Zhang, Guido Salvaneschi, Andrew C. Myers

Proceedings of the ACM on Programming Languages 4 (OOPSLA), 2020

Abstract

Pressed by the difficulty of writing asynchronous, event-driven code, mainstream languages have recently been building in support for a variety of advanced control-flow features. Meanwhile, experimental language designs have suggested effect handlers as a unifying solution to programmer-defined control effects, subsuming exceptions, generators, and async–await. However, despite these trends, complex control flow—in particular, control flow that exhibits a bidirectional pattern—remains challenging to manage.
We introduce bidirectional algebraic effects, a new programming abstraction that supports bidirectional control transfer in a more natural way. Handlers of bidirectional effects can raise further effects to transfer control back to the site where the initiating effect was raised, and can use themselves to handle their own effects. We present applications of this expressive power, which falls out naturally as we push toward the unification of effectful programming with object-oriented programming. We pin down the mechanism and the unification formally using a core language that makes generalizations to effect operations and effect handlers.
The usual propagation semantics of control effects such as exceptions conflicts with modular reasoning in the presence of effect polymorphism—it breaks parametricity. Bidirectionality exacerbates the problem. Hence, we set out to show the core language, which builds on the existing tunneling semantics for algebraic effects, is not only type-safe (no effects go unhandled), but also abstraction-safe (no effects are accidentally handled). We devise a step-indexed logical-relations model, and construct its parametricity and soundness proofs. These core results are fully mechanized in Coq. While a full-featured compiler is left to future work, experiments show that as a first-class language feature, bidirectional handlers can be implemented efficiently.
SuperCompCloud
ScalaLoci

Leveraging Hybrid Cloud HPC with Multitier Reactive Programming

Daniel Sokolowski, Jan-Patrick Lehr, Christian Bischof, Guido Salvaneschi

In Proceedings of the 3rd IEEE/ACM International Workshop on Interoperability of Supercomputing and Cloud Technologies, SuperCompCloud, 2020

Abstract PDF

The advent of cloud computing has enabled large-scale availability of on-demand computing and storage resources. However, these benefits are not yet at the fingertips of HPC developers: Typical HPC applications use on-premise computing resources and rely on static deployment setups, reliable hardware, and rather homogeneous resources. This hinders (partial) execution in the cloud, even though applications could benefit from scaling beyond on-premise resources and from the variety of hardware available in the cloud to speed up execution.
To address this issue, we orchestrate computationally intensive kernels using a high-level programming language that ensures advanced optimization and improves execution flexibility-enabling hybrid cloud/on-premise HPC deployments. Our approach is based on multitier reactive programming, where distributed code is defined within the same compilation unit and computations are placed explicitly using placement types. We adjust placement based on performance characteristics measured before execution, apply our approach to a shortest vector problem (SVP) solver from cryptanalysis, and evaluate it to be effective.
OOPSLA
ConSysT

Rethinking Safe Consistency in Distributed Object-Oriented Programming

Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 4 (OOPSLA), 2020

Abstract PDF

Large scale distributed systems require to embrace the trade off between consistency and availability, accepting lower levels of consistency to guarantee higher availability. Existing programming languages are, however, agnostic to this compromise, resulting in consistency guarantees that are the same for the whole application and are implicitly adopted from the middleware or hardcoded in configuration files.
In this paper, we propose to integrate availability in the design of an object-oriented language, allowing developers to specify different consistency and isolation constraints in the same application at the granularity of single objects. We investigate how availability levels interact with object structure and define a type system that preserves correct program behavior. Our evaluation shows that our solution performs efficiently and improves the design of distributed applications.
CSUR
ScalaLoci

A Survey of Multitier Programming

Pascal Weisenburger, Johannes Wirth, Guido Salvaneschi

ACM Computing Surveys 53 (4), 2020

Abstract PDF

Multitier programming deals with developing the components that pertain to different tiers in the system (e.g., client and server), mixing them in the same compilation unit. In this paradigm, the code for different tiers is then either generated at run time or it results from the compiler splitting the codebase into components that belong to different tiers based on user annotations, static analysis, types, or a combination of these. In the Web context, multitier languages aim at reducing the distinction between client and server code, by translating the code that is to be executed on the clients to JavaScript or by executing JavaScript on the server, too. Ultimately, the goal of the multitier approach is to improve program comprehension, simplify maintenance and enable formal reasoning about the properties of the whole distributed application.
A number of multitier research languages have been proposed over the last decade, which support various degrees of multitier programming and explore different design tradeoffs. In this article, we provide an overview of the existing solutions, discuss their positioning in the design space, and outline open research problems.
ISSTA

A Programming Model for Semi-Implicit Parallelization of Static Analyses

Dominik Helm, Florian Kübler, Jan Thomas Kölzer, Philipp Haller, Michael Eichberg, Guido Salvaneschi, Mira Mezini

In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA, 2020

Abstract

Parallelization of static analyses is necessary to scale to real-world programs, but it is a complex and difficult task and, therefore, often only done manually for selected high-profile analyses. In this paper, we propose a programming model for semi-implicit parallelization of static analyses which is inspired by reactive programming. Reusing the domain-expert knowledge on how to parallelize anal- yses encoded in the programming framework, developers do not need to think about parallelization and concurrency issues on their own. The programming model supports stateful computations, only requires monotonic computations over lattices, and is independent of specific analyses. Our evaluation shows the applicability of the programming model to different analyses and the importance of user-selected scheduling strategies. We implemented an IFDS solver that was able to outperform a state-of-the-art, specialized parallel IFDS solver both in absolute performance and scalability.
FTfJP
ConSysT

ConSysT: Tunable, Safe Consistency Meets Object-Oriented Programming

Mirko Köhler, Nafise Eskandani, Alessandro Margara, Guido Salvaneschi

In Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP, 2020

Abstract

Data replication is essential in scenarios like geo-distributed datacenters, but poses challenges for data consistency. Developers adopt Strong consistency at the cost of performance or embrace Weak consistency and face a higher programming complexity. We argue that languages should associate consistency to data types. We present , a programming language and middleware that provides abstractions to specify consistency types, enabling mixing different consistency levels in the same application. Such mechanism is fully integrated with object-oriented programming and type system guarantees that different levels can only be mixed correctly.
‹Programming›
ScalaLoci

Implementing a Language for Distributed Systems: Choices and Experiences with Type Level and Macro Programming in Scala

Pascal Weisenburger, Guido Salvaneschi

The Art, Science, and Engineering of Programming 4 (3), 2020

Abstract PDF Code Website

Multitier programming languages reduce the complexity of developing distributed systems by developing the distributed system in a single coherent code base. The compiler or the runtime separate the code for the components of the distributed system, enabling abstraction over low level implementation details such as data representation, serialization and network protocols. Our ScalaLoci language allows developers to declare the different components and their architectural relation at the type level, allowing static reasoning about about distribution and remote communication and guaranteeing static type safety across components. The compiler splits the multitier program into the component-specific code and automatically generates the communication boilerplate. Communication between components can be modeled by declaratively specifying data flows between components using reactive programming.
In this paper, we report on the implementation of our design and our experience with embedding our language features into Scala as a host language. We show how a combination of Scala’s advanced type level programming and its macro system can be used to enrich the language with new abstractions. We comment on the challenges we encountered and the solutions we developed for our current implementation and outline suggestions for an improved macro system to support the such use cases of embedding of domain-specific abstractions.
ScalaLoci

A Programming Language for Distributed Systems

Pascal Weisenburger

Doctoral dissertation, Technische Universität Darmstadt, 2020

Abstract

Today’s software, including many everyday services, such as online streaming, search engines and social networks, is widely distributed, running on top of a network of interconnected computers. Such distributed applications are traditionally developed as separate modules for each component in the distributed system. These modules react to events, like user input or messages from the network, and in turn produce new events for the other modules. Separation into different modules is problematic because combining modules is notoriously hard and requires extensive and time-consuming integration and manual implementation of communication forces programmers to program complex event-based communication schemes among hosts ? an activity which is often low-level and error-prone. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole. For these reasons, despite most software today is distributed, the design and development of distributed systems remains surprisingly challenging.
We present the ScalaLoci distributed programming language, our approach for taming the complexity of developing distributed applications via specialized programming language support. ScalaLoci addresses the issues above with a coherent model based on placement types that enables reasoning about distributed data flows otherwise scattered across multiple modules, supporting multiple software architectures via dedicated language features and abstracting over low-level communication details and data conversions.
ScalaLoci does not force developers to modularize software along network boundaries as is traditionally the case when developing distributed systems. Instead, we propose a module system that supports encapsulating each (cross-host) functionality and defining it over abstract peer types. As a result, we disentangle modularization and distribution and we enable the definition of a distributed system as a composition of ScalaLoci modules, each representing a subsystem.
Our case studies on distributed algorithms, distributed data structures, as well as on real-world distributed streaming engines show that ScalaLoci simplifies developing distributed systems, reduces error-prone communication code and favors early detection of bugs. As we demonstrate, the ScalaLoci module system allows the definition of reusable patterns of interaction in distributed software and enables separating the modularization and distribution concerns, properly separating functionalities in distributed systems.

2019

ASE

Automated Refactoring to Reactive Programming

Mirko Köhler, Guido Salvaneschi

In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, ASE, 2019

Abstract PDF

Reactive programming languages and libraries, such as ReactiveX, have been shown to significantly improve software design and have seen important industrial adoption over the last years. Asynchronous applications - which are notoriously error-prone to implement and to maintain - greatly benefit from reactive programming because they can be defined in a declarative style, which improves code clarity and extensibility.
In this paper, we tackle the problem of refactoring existing software that has been designed with traditional abstractions for asynchronous programming. We propose 2Rx, a refactoring approach to automatically convert asynchronous code to reactive programming. Our evaluation on top-starred GitHub projects shows that 2Rx is effective with common asynchronous constructs and it can provide a refactoring for 91.7% of their occurrences.
OOPSLA
REScala

A Fault-Tolerant Programming Model for Distributed Interactive Applications

Ragnar Mogk, Joscha Drechsler, Guido Salvaneschi, Mira Mezini

Proceedings of the ACM on Programming Languages 3 (OOPSLA), 2019

Abstract

Ubiquitous connectivity of web, mobile, and IoT computing platforms has fostered a variety of distributed applications with decentralized state. These applications execute across multiple devices with varying reliability and connectivity. Unfortunately, there is no declarative fault-tolerant programming model for distributed interactive applications with an inherently decentralized system model.
We present a novel approach to automating fault tolerance using high-level programming abstractions tailored to the needs of distributed interactive applications. Specifically, we propose a calculus that enables formal reasoning about applications’ dataflow within and across individual devices. Our calculus reinterprets the functional reactive programming model to seamlessly integrate its automated state change propagation with automated crash recovery of device-local dataflow and disconnection-tolerant distribution with guaranteed automated eventual consistency semantics based on conflict-free replicated datatypes. As a result, programmers are relieved of handling intricate details of distributing change propagation and coping with distribution failures in the presence of interactivity. We also provides proofs of our claims, an implementation of our calculus, and an empirical evaluation using a common interactive application.
SPLASH Companion
ConSysT

Distributed Object-Oriented Programming with Multiple Consistency Levels in ConSysT

Nafise Eskandani, Mirko Köhler, Alessandro Margara, Guido Salvaneschi

In Companion Proceedings of the 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH Companion, 2019

Abstract

Data replication is essential in scenarios like geo-distributed datacenters and edge computing. Yet, it poses a challenge for data consistency. Developers either adopt high consistency at the detriment of performance or they embrace low consistency and face a much higher programming complexity. We argue that language abstractions should support associating the level of consistency to data types. We present ConSysT, a programming language and middleware that provides abstractions to specify consistency types, enabling mixing different consistency levels in the same application. Such mechanism is fully integrated with object-oriented programming and type system guarantees that different levels can be mixed only in a correct way.
REBLS

GRASS: Generic Reactive Application-Specific Scheduling

Marcel Blöcher, Matthias Eichholz, Pascal Weisenburger, Patrick Eugster, Mira Mezini, Guido Salvaneschi

In Proceedings of the 6th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems, REBLS, 2019

Abstract PDF

High resource utilization is important to operate compute infrastructures and data centers efficiently. High utilization is achieved by multiplexing several applications over the same physical infrastructure. Yet, with this approach, the different requirements of each application have to be taken into account when scheduling resources.
We propose GRASS, a reactive domain-specific abstraction that allows specifying application-tailored resource scheduling policies. We demonstrate how the declarative approach of GRASS enables extension and composition of scheduling policies. Our evaluation shows the performance benefits of considering application-specific information in a composition of scheduling policies that adapt at run time.
OOPSLA

Language-Integrated Privacy-Aware Distributed Queries

Guido Salvaneschi, Mirko Köhler, Daniel Sokolowski, Philipp Haller, Sebastian Erdweg, Mira Mezini

Proceedings of the ACM on Programming Languages 3 (OOPSLA), 2019

Abstract PDF

Distributed query processing is an effective means for processing large amounts of data. To abstract from the technicalities of distributed systems, algorithms for operator placement automatically distribute sequential data queries over the available processing units. However, current algorithms for operator placement focus on performance and ignore privacy concerns that arise when handling sensitive data.
We present a new methodology for privacy-aware operator placement that both prevents leakage of sensitive information and improves performance. Crucially, our approach is based on an information-flow type system for data queries to reason about the sensitivity of query subcomputations. Our solution unfolds in two phases. First, placement space reduction generates deployment candidates based on privacy constraints using a syntax-directed transformation driven by the information-flow type system. Second, constraint solving selects the best placement among the candidates based on a cost model that maximizes performance. We verify that our algorithm preserves the sequential behavior of queries and prevents leakage of sensitive data. We implemented the type system and placement algorithm for a new query language SecQL and demonstrate significant performance improvements in benchmarks.
REBLS
ScalaLoci

Multitier Reactive Programming in High Performance Computing

Daniel Sokolowski, Philipp Martens, Guido Salvaneschi

Presentation at the 6th Workshop on Reactive and Event-based Languages and Systems (REBLS), 2019

Abstract PDF

High Performance Computing (HPC) is crucial in a number of sectors, including weather forecasts, particle simulations and fluid dynamics. Existing programming frameworks for HPC expose developers to low-level details such as message passing and explicit memory management, which are hard to program and error-prone.
In this paper, we present ongoing work on increasing the level of abstraction for HPC. We tackle this problem with an approach based on a combination of multitier programming and reactive programming which enables the development of complex processor configurations in a uniform way using event streams as communication pattern. We report our experience with LULESH, a well known HPC benchmark, and we outline our research roadmap.
GHTC

Smart Street Lights and Mobile Citizen Apps for Resilient Communication in a Digital City

Lars Baumgärtner, Jonas Höchst, Patrick Lampe, Ragnar Mogk, Artur Sterz, Pascal Weisenburger, Mira Mezini, Bernd Freisleben

In Proceedings of the 2019 IEEE Global Humanitarian Technology Conference, GHTC, 2019

Abstract PDF

While information and communication technology is crucial for the operation of urban infrastructures and the well-being of its inhabitants, current technology is quite vulnerable to disruptions of various kinds. In future smart cities, a more resilient urban infrastructure is imperative to handle the increasing number of hazardous situations. We present a novel resilient communication approach based on smart street lights as part of the public infrastructure. It supports people in their everyday life and adapts its functionality to the challenges of emergency situations. Our approach relies on various environmental sensors and in-situ processing for automatic situation assessment, and a range of communication mechanisms for maintaining a communication network. Furthermore, resilience is not only achieved based on infrastructure deployed by a digital city’s municipality, but also based on integrating citizens through software that runs on their mobile devices. Web-based zero-installation and platform-agnostic apps can switch to device-to-device communication to continue benefiting people even during a disaster situation. Our approach, featuring a covert channel for professional responders and a zero-installation app, is evaluated through a prototypical implementation based on a commercially available street light.
ECOOP

How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4

Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, Mira Mezini

In Proceedings of the 33rd European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2019

Abstract

The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last few years, experience with an increasing number of programs has shown the risks of the unsafe approach, which often leads to subtle software bugs.
This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity – a common source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our evaluation shows that SafeP4’s type system can effectively eliminate common failures in many real-world programs.
ECOOP
ScalaLoci

Multitier Modules

Pascal Weisenburger, Guido Salvaneschi

In Proceedings of the 33rd European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2019

Abstract PDF Code Website

Multitier programming languages address the complexity of developing distributed systems abstracting over low level implementation details such as data representation, serialization and network protocols. Since the functionalities of different peers can be defined in the same compilation unit, multitier languages do not force developers to modularize software along network boundaries. Unfortunately, combining the code for all tiers into the same compilation unit poses a scalability challenge or forces developers to resort to traditional modularization abstractions that are agnostic to the multitier nature of the language.
In this paper, we address this issue with a module system for multitier languages. Our module system supports encapsulating each (cross-peer) functionality and defining it over abstract peer types. As a result, we disentangle modularization and distribution and we enable the definition of a distributed system as a composition of multitier modules, each representing a subsystem. Our case studies on distributed algorithms, distributed data structures, as well as on the Apache Flink task distribution system, show that multitier modules allow the definition of reusable (abstract) patterns of interaction in distributed software and enable separating the modularization and distribution concerns, properly separating functionalities in distributed systems.
CoRR

Type-safe, Polyvariadic Event Correlation

Oliver Bračevac, Guido Salvaneschi, Sebastian Erdweg, Mira Mezini

arXiv, 2019

Abstract

The pivotal role that event correlation technology plays in todays applications has lead to the emergence of different families of event correlation approaches with a multitude of specialized correlation semantics, including computation models that support the composition and extension of different semantics.
However, type-safe embeddings of extensible and composable event patterns into statically-typed generalpurpose programming languages have not been systematically explored so far. This is unfortunate, as typesafe embedding of event patterns is important to enable increased correctness of event correlation computations as well as domain-specific optimizations. Event correlation technology has often adopted well-known and intuitive notations from database queries, for which approaches to type-safe embedding do exist. However, we argue in the paper that these approaches, which are essentially descendants of the work on monadic comprehensions, are not well-suited for event correlations and, thus, cannot without further ado be reused/repurposed for embedding event patterns.
To close this gap we propose PolyJoin, a novel approach to type-safe embedding for fully polyvariadic event patterns with polymorphic correlation semantics. Our approach is based on a tagless final encoding with uncurried higher-order abstract syntax (HOAS) representation of event patterns withn variables, for arbitrary n ∈ ℕ. Thus, our embedding is defined in terms of the host language without code generation and exploits the host language type system to model and type check the type system of the pattern language. Hence, by construction it impossible to define ill-typed patterns. We show that it is possible to have a purely library-level embedding of event patterns, in the familiar join query notation, which is not restricted to monads. PolyJoin is practical, type-safe and extensible. An implementation of it in pure multicore OCaml is readily usable.
FAS*W

On Context-Orientation in Aggregate Programming

Roberto Casadei, Danilo Pianini, Guido Salvaneschi, Mirko Viroli

In Proceedings of the 2019 IEEE 4th International Workshops on Foundations and Applications of Self* Systems, FAS*W, 2019

Abstract

Context-awareness plays a central role in selfadaptive software. By a programming perspective, context is often used implicitly, and context-aware code is fragmented in the codebase. In Context-Oriented Programming, instead, context is considered a first-class citizen and is explicitly used to modularise context-sensitive functionality and behavioural variability. In this paper, we reflect on the role of context in collective adaptive systems, by a discussion from the special perspective of a macro paradigm, Aggregate Programming, which supports the specification of collective behaviour by a global perspective through functional compositions of field computations. In particular, we consider the abstractions exposed in Context-Oriented and Aggregate Programming, suggest potential synergies in both directions, and accordingly take the first steps towards a combined design
DEBS
ScalaLoci

Tutorial: Developing Distributed Systems with Multitier Programming

Pascal Weisenburger, Guido Salvaneschi

In Proceedings of the 13th ACM International Conference on Distributed and Event-Based Systems, DEBS, 2019

Abstract PDF

Developing distributed systems is a complex task that requires to program different peers, often using several languages on different platforms, writing communication code and handling data serialization and conversion.
We show how the multitier programming paradigm can alleviate these issues, supporting a development model where all peers in the system can be written in the same language and coexist in the same compilation units, communication code is automatically inserted by the compiler and the language abstracts over data conversion and serialization. We present multitier programming abstractions, discuss their applicability step by step for the development of small applications and discuss larger case studies on distributed stream processing, like Apache Flink and Apache Gearpump.
PASS
J_E

Language Support for Multiple Privacy Enhancing Technologies

Aditya Oak, Mira Mezini, Guido Salvaneschi

In Companion Proceedings of the 3rd International Conference on Art, Science, and Engineering of Programming, ‹Programming› Companion, 2019

Abstract

Privacy is one of the critical aspects in the design of computing systems. Various techniques are being used to enforce privacy, such as information flow control, symmetric/asymmetric cryptography, secure computing enclaves, partial homomorphic encryption and differential privacy. These mechanisms should ideally be combined in complex software systems as they offer different properties and performance trade offs. Unfortunately, reasoning about the privacy properties of such combination is still an open research problem.
In this paper, we present our vision on a programming language in which we incorporate different privacy preservation techniques in a common programming model.

2018

OOPSLA
ScalaLoci

Distributed System Development with ScalaLoci

Pascal Weisenburger, Mirko Köhler, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 2 (OOPSLA), 2018

Abstract PDF Code Website

Distributed applications are traditionally developed as separate modules, often in different languages, which react to events, like user input, and in turn produce new events for the other modules. Separation into components requires time-consuming integration. Manual implementation of communication forces programmers to deal with low-level details. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole. The ScalaLoci distributed programming language addresses these issues with a coherent model based on placement types that enables reasoning about distributed data flows, supporting multiple software architectures via dedicated language features and abstracting over low-level communication details and data conversions. As we show, ScalaLoci simplifies developing distributed systems, reduces error-prone communication code and favors early detection of bugs.
OOPSLA
REScala

Thread-Safe Reactive Programming

Joscha Drechsler, Ragnar Mogk, Guido Salvaneschi, Mira Mezini

Proceedings of the ACM on Programming Languages 2 (OOPSLA), 2018

Abstract PDF

The execution of an application written in a reactive language involves transfer of data and control flow between imperative and reactive abstractions at well-defined points. In a multi-threaded environment, multiple such interactions may execute concurrently, potentially causing data races and event ordering ambiguities. Existing RP languages either disable multi-threading or handle it at the cost of reducing expressiveness or weakening consistency. This paper proposes a model for thread-safe reactive programming (RP) that ensures abort-free strict serializability under concurrency while sacrificing neither expressiveness nor consistency. We also propose an architecture for integrating a corresponding scheduler into the RP language runtime, such that thread-safety is provided "out-of-the-box" to the applications.
We show the feasibility of our proposal by providing and evaluating a ready-to-use implementation integrated into the REScala programming language. The scheduling algorithm is formally proven correct. A thorough empirical evaluation shows that reactive applications build on top of it scale with multiple threads, while the scheduler incurs acceptable performance overhead in a single-threaded configuration. The scalability enabled by our scheduler is roughly on-par with that of hand-crafted application-specific locking and better than the scalability enabled by a scheduler using an off-the-shelf software transactional memory library.
ECOOP
REScala

Fault-tolerant Distributed Reactive Programming

Ragnar Mogk, Lars Baumgärtner, Guido Salvaneschi, Bernd Freisleben, Mira Mezini

In Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2018

Abstract PDF

In this paper, we present a holistic approach to provide fault tolerance for distributed reactive programming. Our solution automatically stores and recovers program state to handle crashes, automatically updates and shares distributed parts of the state to provide eventual consistency, and handles errors in a fine-grained manner to allow precise manual control when necessary. By making use of the reactive programming paradigm, we provide these mechanisms without changing the behavior of existing programs and with reasonable performance, as indicated by our experimental evaluation.
SOAP

Lattice Based Modularization of Static Analyses

Michael Eichberg, Florian Kübler, Dominik Helm, Michael Reif, Guido Salvaneschi, Mira Mezini

In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, ISSTA/ECOOP Companion, 2018

Abstract

Static analyses which compute conceptually independent information, e.g., class immutability or method purity are typically developed as standalone, closed analyses. Complementary information that could improve the analyses is either ignored by making a sound over-approximation or it is also computed by the analyses, but at a rudimentary level. For example, an immutability analysis requires field mutability information, alias/escape information, and information about the concurrent behavior of methods to correctly classify classes like java.lang.String or java.util.BigDecimal. As a result, without properly supporting the integration of independently developed, mutually benefiting analysis, many analyses will not correctly classify relevant entities.We propose to use explicitly reified lattices that encode the information about a source code element’s properties (e.g., a method’s purity or a class’ immutability) as the sole interface between mutually dependent analyses. This enables the composition of multiple analyses. Our case study shows that using such an approach enables highly scalable, lightweight implementations of modularized static analyses.
FTfJP
ScalaLoci

Static Latency Tracking with Placement Types

Pascal Weisenburger, Tobias Reinhard, Guido Salvaneschi

In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, ISSTA/ECOOP Companion, 2018

Abstract PDF

Large-scale distributed applications, e.g., in geodistributed data centers, pose a performance challenge to developers which need to take high cross-data-center latency communication cost into account. We present a preliminary investigation of a type system that tracks latency and makes the cost of remote calls explicit, raising developers’ awareness of communication overhead.
ICFP

Versatile Event Correlation with Algebraic Effects

Oliver Bračevac, Nada Amin, Guido Salvaneschi, Sebastian Erdweg, Patrick Eugster, Mira Mezini

Proceedings of the ACM on Programming Languages 2 (ICFP), 2018

Abstract PDF

We present the first language design to uniformly express variants of n-way joins over asynchronous event streams from different domains, e.g., stream-relational algebra, event processing, reactive and concurrent programming. We model asynchronous reactive programs and joins in direct style, on top of algebraic effects and handlers. Effect handlers act as modular interpreters of event notifications, enabling fine-grained control abstractions and customizable event matching. Join variants can be considered as cartesian product computations with “degenerate” control flow, such that unnecessary tuples are not materialized a priori. Based on this computational interpretation, we decompose joins into a generic, naïve enumeration procedure of the cartesian product, plus variant-specific extensions, represented in terms of user-supplied effect handlers. Our microbenchmarks validate that this extensible design avoids needless materialization. Alongside a formal semantics for joining and prototypes in Koka and multicore OCaml, we contribute a systematic comparison of the covered domains and features.
DEBS

Multimodal Complex Event Processing on Mobile Devices

Pablo Graubner, Christoph Thelen, Michael Körber, Artur Sterz, Guido Salvaneschi, Mira Mezini, Bernhard Seeger, Bernd Freisleben

In Proceedings of the 12th ACM International Conference on Distributed and Event-Based Systems, DEBS, 2018

Abstract

Mobile devices are increasingly being used in edge and fog computing environments to process contextual data collected by sensors. Although complex event processing (CEP) is a suitable approach for realizing context-aware services on mobile devices in these environments, existing mobile CEP engines do not leverage the full potential of modern mobile hardware/software architectures. In this paper, we present multimodal CEP, a novel approach to process streams of events on-device in user space (user mode), in the operating system (kernel mode), on the Wi-Fi chip (Wi-Fi mode), and/or on a sensor hub (hub mode), providing significant improvements in terms of power consumption and throughput. Multimodal CEP automatically breaks up CEP queries and selects the most adequate execution mode for the involved CEP operators. Filter, aggregation, and correlation operators can be expressed in a high-level language without requiring system-level domain-specific knowledge. Multimodal CEP enables developers to efficiently detect user activities, collect environmental conditions, or interpret operating system and network events. Furthermore, it facilitates novel context-aware services, demonstrated by a use case for gathering and analyzing mobility data by Wi-Fi probe request tracking.
DEBS

TCEP: Adapting to Dynamic User Environments by Enabling Transitions between Operator Placement Mechanisms

Manisha Luthra, Boris Koldehofe, Pascal Weisenburger, Guido Salvaneschi, Raheel Arif

In Proceedings of the 12th ACM International Conference on Distributed and Event-Based Systems, DEBS, 2018

Abstract PDF

Operator placement has a profound impact on the performance of a distributed complex event processing system (DCEP). Since the behavior of a placement mechanism strongly depends on its environment; a single placement mechanism is often not enough to fulfill stringent performance requirements under environmental changes. In this paper, we show how DCEP can benefit from the adaptive use of multiple placement mechanisms. We propose TCEP, a DCEP system to integrate multiple placement mechanisms. By enabling transitions, TCEP can seamlessly exchange distinct operator mechanisms at runtime. We make two main contributions that are highly important for a cost-efficient transition: i) a transition strategy for efficiently scheduling state migrations and ii) a lightweight learning algorithm to adaptively select an appropriate placement mechanism as a consequence of a transition. Our evaluations for important decentralized placement mechanisms in the context of an IoT scenario show that transitions can better fulfill QoS demands in a dynamic environment. Thereby efficient scheduling of state migrations can help to faster complete transitions by up to 94%.
TSE

On the Semantics of Distributed Reactive Programming: The Cost of Consistency

Alessandro Margara, Guido Salvaneschi

IEEE Transactions on Software Engineering 44 (7), 2018

Abstract

The reactive programming paradigm aims to simplify the development of reactive systems. It provides abstractions to define time-changing values that are automatically updated by the runtime according to their dependencies. The benefits of reactive programming in distributed settings have been recognized for long. Yet, existing solutions for distributed reactive programming enforce the same semantics as in single processes, introducing communication and synchronization costs that hamper scalability. Establishing suitable abstractions for distributed reactive programming demands for a deeper investigation of the semantics of change propagation. This paper takes a foundational approach and defines precise propagation semantics in terms of consistency guarantees that constrain the order and isolation of value updates. We study the benefits and costs of these consistency guarantees both theoretically and empirically, using case studies and synthetic benchmarks. We show that different applications require different levels of consistency and that manually implementing the required level on a middleware that provides a lower one annuls the abstraction improvements of reactive programming. This motivates a framework that enables the developers to select the best trade-off between consistency and overhead for the problem at hand. To this end, we present DREAM, a distributed reactive programming middleware with flexible consistency guarantees.
PX
REScala

Reactive Programming Experience with REScala

Ragnar Mogk, Guido Salvaneschi, Mira Mezini

In Companion Proceedings for the 2nd International Conference on Art, Science, and Engineering of Programming, ‹Programming› Companion, 2018

Abstract

Reactive programming is a recent programming paradigm that specifically targets reactive applications. Over the years, a number of reactive languages have been proposed, with different combinations of features, and various target domains.
Unfortunately, there is a lack of knowledge about the experience of developing software applications with reactive languages. As a result, a number of design choices in reactive programming languages remain disconnected from experience and the applicability of reactive programming to various domains remains unclear.
To bridge this gap, we report on our experience of developing reactive applications as well as teaching reactive programming in REScala, which we collected over several years of research and practice.
PASS

Towards Safe Modular Composition of Network Functions

Matthias Eichholz, Guido Salvaneschi, Mira Mezini

In Companion Proceedings for the 2nd International Conference on Art, Science, and Engineering of Programming, ‹Programming› Companion, 2018

Abstract

Network Function Virtualization (NFV) aims to overcome the limitations of hardware middleboxes by moving network functions to software. Ultimately, this approach enables deployment into virtualized environments with higher flexibility, reducing deployment time and costs. In common industrial practice, multiple smaller network functions are often chained together into service function chains. Yet, service function chains are extremely fragile, lacking basic guarantees on correct composition and dependency reasoning.
In this position paper, we propose a roadmap towards language abstractions that address this issue. We introduce the problems with current service function chaining technology and present the research program we envision.

2017

TSE
REScala

On the Positive Effect of Reactive Programming on Software Comprehension: An Empirical Study

Guido Salvaneschi, Sebastian Proksch, Sven Amann, Sarah Nadi, Mira Mezini

IEEE Transactions on Software Engineering 43 (12), 2017

Abstract PDF

Starting from the first investigations with strictly functional languages, reactive programming has been proposed as the programming paradigm for reactive applications. Over the years, researchers have enriched reactive languages with more powerful abstractions, embedded these abstractions into mainstream languages—including object-oriented languages—and applied reactive programming to several domains, such as GUIs, animations, Web applications, robotics, and sensor networks. However, an important assumption behind this line of research is that, beside other claimed advantages, reactive programming makes a wide class of otherwise cumbersome applications more comprehensible. This claim has never been evaluated. In this paper, we present the first empirical study that evaluates the effect of reactive programming on comprehension. The study involves 127 subjects and compares reactive programming to the traditional object-oriented style with the Observer design pattern. Our findings show that program comprehension is significantly enhanced by the reactive-programming paradigm—a result that suggests to further develop research in this field.
FTfJP
ConSysT

Consistency Types for Safe and Efficient Distributed Programming

Alessandro Margara, Guido Salvaneschi

In Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs, FTfJP, 2017

Abstract PDF

Consistency is a long standing problem in distributed systems. Low consistency levels are considered a necessity for scalability. High consistency is required for critical tasks such as payment and identification. Modern (geo-)distributed systems rely on the data propagation mechanisms and consistency guarantees of the distributed data store they build upon, which makes the implementation of a system that mixes different levels of consistency complex and error prone. In this paper we present preliminary work on ConSysT, a programming language that supports heterogeneous consistency specifications at the type level. In ConSysT, developers assign consistency levels directly to the data and the type system ensures the correct behavior of the application even with computations that mix data at multiple consistency levels. Our vision is that the ConSysT runtime automatically determines the most efficient mechanism to achieve the desired level of consistency among those offered by the underlying data store.
SEAMS

Quality-Aware Runtime Adaptation in Complex Event Processing

Pascal Weisenburger, Manisha Luthra, Boris Koldehofe, Guido Salvaneschi

In Proceedings of the 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS, 2017

Abstract PDF

Complex event processing (CEP) is a fundamental paradigm for a software system to self-adapt to environmental changes. CEP provides efficient means to detect (complex) events corresponding to environmental changes by performing a real-time analysis on many, possibly heterogeneous, data sources. The way current CEP systems detect events is determined at design time without accounting for dynamic changes of the environment monitored by the CEP system. This can lead to situations where the performance, quality and reliability of event detection significantly drop (e.g., due to mobility) since initial assumptions of the environment are violated or stated too general. In this paper, we propose AdaptiveCEP, a CEP system that is able to self-adapt to detected changes in environmental conditions. We propose a CEP query language that allows specifying changes in the behavior of the CEP system and its mechanisms in detecting events dependent on environmental conditions. This way, AdaptiveCEP can select the best-suited configurations for given quality demands. In our evaluation, we show by means of a reference concept how the flexibility exposed by the query language helps to achieve significant performance gains.

2016

SPLASH DS
ScalaLoci

Multitier Reactive Abstractions

Pascal Weisenburger

In Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH Companion, 2016

Abstract PDF

Distributed applications are traditionally developed using separate modules for each component in the distributed system, which can even be written in different programming languages. Those modules react on events such as user input, which are produced by other modules, and may in turn produce new events to be handled by different modules. Thus, most distributed applications are reactive in nature. Distributed event-based data flow makes it is hard to reason about the system and therefore makes the development of distributed systems challenging.
In this paper, we present language abstractions for distributed reactive programming easing the development of such applications and supporting various distributed architectures.
SCALA

Reactive Async: Expressive Deterministic Concurrency

Philipp Haller, Simon Geries, Michael Eichberg, Guido Salvaneschi

In Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala, SCALA, 2016

Abstract PDF

Concurrent programming is infamous for its difficulty. An important source of difficulty is non-determinism, stemming from unpredictable interleavings of concurrent activities. Futures and promises are widely-used abstractions that help designing deterministic concurrent programs, although this property cannot be guaranteed statically in mainstream programming languages. Deterministic-by-construction concurrent programming models avoid this issue, but they typically restrict expressiveness in important ways.
This paper introduces a concurrent programming model, Reactive Async, which decouples concurrent computations using so-called cells, shared locations which generalize futures as well as recent deterministic abstractions such as LVars. Compared to previously proposed programming models Reactive Async provides (a) a fallback mechanism for the case where no computation ever computes the value of a given cell, and (b) explicit and optimized handling of cyclic dependencies. We present a complete implementation of the Reactive Async programming model as a library in Scala. Finally, the paper reports on a case study applying Reactive Async to static analyses of JVM bytecode based on the Opal framework.
SCALA

SecureScala: Scala Embedding of Secure Computations

Markus Hauck, Savvas Savvides, Patrick Eugster, Mira Mezini, Guido Salvaneschi

In Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala, SCALA, 2016

Abstract PDF

Cloud computing offers an attractive and cost-efficient computing platform and hence it has been widely adopted by the industry and the government. At the same time, cloud computing poses a serious security challenge because sensitive data must often be outsourced to third party entities that can access the data and perform computations on them.
Partial homomorphic encryption is promising for secure computation, since it allows programs to be executed over encrypted data. Despite advances in cryptographic techniques have improved the expressivity of such programs, integration with mainstream languages has seen little progress. To this end, we present SecureScala, a domain-specific language in Scala that allows expressing secure programs without requiring any cryptographic knowledge. SecureScala is based on a novel combination of free monads and free applicative functors and supports parallel execution and static analyzability. We evaluate our approach through several case studies, demonstrate its expressivity, and show that it incurs in limited performance overhead.
PLATEAU
REScala

What Do We Really Know about Data Flow Languages?

Guido Salvaneschi

In Proceedings of the 7th International Workshop on Evaluation and Usability of Programming Languages and Tools, PLATEAU, 2016

Abstract PDF

Over the last years, a number of languages based on data flow abstractions have been proposed in different important areas including Big Data, stream processing, reactive programming, real time analytics. While there is a general agreement that the data flow style simplifies the access to such complex systems compared to low level imperative APIs, this design has been substantiated by little evidence.
In this paper, we advocate a systematic investigation of the design principles of data flow languages and suggest important research questions that urge to be addressed.
PLDI

Accepting Blame for Safe Tunneled Exceptions

Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, Andrew C. Myers

In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, 2016

Abstract

Unhandled exceptions crash programs, so a compile-time check that exceptions are handled should in principle make software more reliable. But designers of some recent languages have argued that the benefits of statically checked exceptions are not worth the costs. We introduce a new statically checked exception mechanism that addresses the problems with existing checked-exception mechanisms. In particular, it interacts well with higher-order functions and other design patterns. The key insight is that whether an exception should be treated as a "checked" exception is not a property of its type but rather of the context in which the exception propagates. Statically checked exceptions can "tunnel" through code that is oblivious to their presence, but the type system nevertheless checks that these exceptions are handled. Further, exceptions can be tunneled without being accidentally caught, by expanding the space of exception identifiers to identify the exception-handling context. The resulting mechanism is expressive and syntactically light, and can be implemented efficiently. We demonstrate the expressiveness of the mechanism using significant codebases and evaluate its performance. We have implemented this new exception mechanism as part of the new Genus programming language, but the mechanism could equally well be applied to other programming languages.
ICSE
REScala

Debugging for Reactive Programming

Guido Salvaneschi, Mira Mezini

In Proceedings of the 38th International Conference on Software Engineering, ICSE, 2016

Abstract PDF

Reactive programming is a recent programming technique that provides dedicated language abstractions for reactive software. Reactive programming relieves developers from manually updating outputs when the inputs of a computation change, it overcomes a number of well-know issues of the Observer design pattern, and it makes programs more comprehensible. Unfortunately, complementing the new paradigm with proper tools is a vastly unexplored area. Hence, as of now, developers can embrace reactive programming only at the cost of a more challenging development process.
In this paper, we investigate a primary issue in the field: debugging programs in the reactive style. We analyze the problem of debugging reactive programs, show that the reactive style requires a paradigm shift in the concepts needed for debugging, and propose RP Debugging, a methodology for effectively debugging reactive programs. These ideas are implemented in Reactive Inspector, a debugger for reactive programs integrated with the Eclipse Scala IDE. Evaluation based on a controlled experiment shows that RP Debugging outperforms traditional debugging techniques.
ICSE Companion
REScala

Debugging Reactive Programming with Reactive Inspector

Guido Salvaneschi, Mira Mezini

In Companion Proceedings of the 38th International Conference on Software Engineering, ICSE Companion, 2016

Abstract PDF

Reactive programming provides dedicated language abstractions for reactive software, relieving developers from manually updating outputs when the inputs of a computation change. Unfortunately, complementing the new paradigm with proper tools that support coding activities is a vastly unexplored area.
We investigate a primary issue in the field: debugging programs in the reactive style. We propose RP Debugging, a methodology for effectively debugging reactive programs. These ideas are implemented in Reactive Inspector, a debugger for reactive programs integrated with the Eclipse Scala development environment.
MODULARITY

CPL: A Core Language for Cloud Computing

Oliver Bračevac, Sebastian Erdweg, Guido Salvaneschi, Mira Mezini

In Proceedings of the 15th International Conference on Modularity, MODULARITY, 2016

Abstract PDF

Running distributed applications in the cloud involves deployment. That is, distribution and configuration of application services and middleware infrastructure. The considerable complexity of these tasks resulted in the emergence of declarative JSON-based domain-specific deployment languages to develop deployment programs. However, existing deployment programs unsafely compose artifacts written in different languages, leading to bugs that are hard to detect before run time. Furthermore, deployment languages do not provide extension points for custom implementations of existing cloud services such as application-specific load balancing policies.
To address these shortcomings, we propose CPL (Cloud Platform Language), a statically-typed core language for programming both distributed applications as well as their deployment on a cloud platform. In CPL, application services and deployment programs interact through statically typed, extensible interfaces, and an application can trigger further deployment at run time. We provide a formal semantics of CPL and demonstrate that it enables type-safe, composable and extensible libraries of service combinators, such as load balancing and fault tolerance.

2015

PLDI

Lightweight, Flexible Object-Oriented Generics

Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, Andrew C. Myers

In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, 2015

Abstract PDF

The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report.
SCP

ContextErlang

Guido Salvaneschi, Carlo Ghezzi, Matteo Pradella

Science of Computer Programming 102 (C), 2015

Abstract PDF

Self-adaptive software modifies its behavior at run time to satisfy changing requirements in a dynamic environment. Context-oriented programming (COP) has been recently proposed as a specialized programming paradigm for context-aware and adaptive systems. COP mostly focuses on run time adaptation of the application’s behavior by supporting modular descriptions of behavioral variations. However, self-adaptive applications must satisfy additional requirements, such as distribution and concurrency, support for unforeseen changes and enforcement of correct behavior in the presence of dynamic change. Addressing these issues at the language level requires a holistic design that covers all aspects and takes into account the possibly cumbersome interaction of those features, for example concurrency and dynamic change.
We present ContextErlang, a COP programming language in which adaptive abstractions are seamlessly integrated with distribution and concurrency. We define ContextErlang’s formal semantics, validated through an executable prototype, and we show how it supports formal proofs that the language design ensures satisfaction of certain safety requirements. We provide empirical evidence that ContextErlang is an effective solution through case studies and a performance assessment. We also show how the same design principles that lead to the development of ContextErlang can be followed to systematically design contextual extensions of other languages. A concrete example is presented concerning ContextScala.
ICSE
REScala

Reactive Programming: A Walkthrough

Guido Salvaneschi, Alessandro Margara, Giordano Tamburrelli

In Proceedings of the 37th International Conference on Software Engineering, ICSE, 2015

Abstract PDF

Over the last few years, Reactive Programming has emerged as the trend to support the development of reactive software through dedicated programming abstractions. Reactive Programming has been increasingly investigated in the programming languages community and it is now gaining the interest of practitioners. Conversely, it has received so far less attention from the software engineering community.
This technical briefing bridges this gap through an accurate overview of Reactive Programming, discussing the available frameworks and outlining open research challenges with an emphasis on cross-field research opportunities.

2014

FSE
REScala

An Empirical Study on Program Comprehension with Reactive Programming

Guido Salvaneschi, Sven Amann, Sebastian Proksch, Mira Mezini

In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE, 2014

Abstract PDF

Starting from the first investigations with strictly functional languages, reactive programming has been proposed as THE programming paradigm for reactive applications. The advantages of designs based on this style over designs based on the Observer design pattern have been studied for a long time. Over the years, researchers have enriched reactive languages with more powerful abstractions, embedded these abstractions into mainstream languages – including object-oriented languages – and applied reactive programming to several domains, like GUIs, animations, Web applications, robotics, and sensor networks.
However, an important assumption behind this line of research – that, beside other advantages, reactive programming makes a wide class of otherwise cumbersome applications more comprehensible – has never been evaluated. In this paper, we present the design and the results of the first empirical study that evaluates the effect of reactive programming on comprehensibility compared to the traditional object-oriented style with the Observer design pattern. Results confirm the conjecture that comprehensibility is enhanced by reactive programming. In the experiment, the reactive programming group significantly outperforms the other group.
OOPSLA
REScala

Distributed REScala: An Update Algorithm for Distributed Reactive Programming

Joscha Drechsler, Guido Salvaneschi, Ragnar Mogk, Mira Mezini

In Proceedings of the 2014 ACM International Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA, 2014

Abstract PDF

Reactive programming improves the design of reactive applications by relocating the logic for managing dependencies between dependent values away from the application logic to the language implementation. Many distributed applications are reactive. Yet, existing change propagation algorithms are not suitable in a distributed setting.
We propose Distributed REScala, a reactive language with a change propagation algorithm that works without centralized knowledge about the topology of the dependency structure among reactive values and avoids unnecessary propagation of changes, while retaining safety guarantees (glitch freedom). Distributed REScala enables distributed reactive programming, bringing the benefits of reactive programming to distributed applications. We demonstrate the enabled design improvements by a case study. We also empirically evaluate the performance of our algorithm in comparison to other algorithms in a simulated distributed setting.
OOPSLA

i3QL: Language-Integrated Live Data Views

Ralf Mitschke, Sebastian Erdweg, Mirko Köhler, Mira Mezini, Guido Salvaneschi

In Proceedings of the 2014 ACM International Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA, 2014

Abstract PDF

An incremental computation updates its result based on a change to its input, which is often an order of magnitude faster than a recomputation from scratch. In particular, incrementalization can make expensive computations feasible for settings that require short feedback cycles, such as interactive systems, IDEs, or (soft) real-time systems.
This paper presents i3QL, a general-purpose programming language for specifying incremental computations. i3QL provides a declarative SQL-like syntax and is based on incremental versions of operators from relational algebra, enriched with support for general recursion. We integrated i3QL into Scala as a library, which enables programmers to use regular Scala code for non-incremental subcomputations of an i3QL query and to easily integrate incremental computations into larger software projects. To improve performance, i3QL optimizes user-defined queries by applying algebraic laws and partial evaluation. We describe the design and implementation of i3QL and its optimizations, demonstrate its applicability, and evaluate its performance.
Software

Programming with Implicit Flows

Guido Salvaneschi, Patrick Eugster, Mira Mezini

IEEE Software 31 (5), 2014

Abstract PDF

Modern software differs significantly from traditional computer applications that mostly process reasonably small amounts of static input data-sets in batch mode. Modern software increasingly processes massive amounts of data, whereby it is also often the case that new input data is produced and/or existing data is modified on the fly. Consequently, programming models that facilitate the development of such software are emerging. What characterizes them is that data, respectively changes thereof, implicitly flow through computation modules. The software engineer declaratively defines computations as compositions of other computations without explicitly modeling how data should flow along dependency relations between data producer and data consumer modules, letting the runtime to automatically manage and optimize data flows.
DEBS
ConSysT

We Have a DREAM: Distributed Reactive Programming with Consistency Guarantees

Alessandro Margara, Guido Salvaneschi

In Proceedings of the 8th ACM International Conference on Distributed Event-Based Systems, DEBS, 2014

Abstract PDF

The reactive programming paradigm has been proposed to simplify the development of reactive systems. It relies on programming primitives to express dependencies between data items and on runtime/middleware support for automated propagation of changes. Despite this paradigm is receiving increasing attention, defining the precise semantics and the consistency guarantees for reactive programming in distributed environments is an open research problem.
This paper targets such problem by studying the consistency guarantees for the propagation of changes in a distributed reactive system. In particular, it introduces three propagation semantics, namely causal, glitch free, and atomic, providing different trade-offs between costs and guarantees. Furthermore, it describes how these semantics are concretely implemented in a Distributed REActice Middleware (DREAM), which exploits a distributed event-based dispatching system to propagate changes.
We compare the performance of DREAM in a wide range of scenarios. This allows us to study the overhead introduced by the different semantics in terms of network traffic and propagation delay and to assess the efficiency of DREAM in supporting distributed reactive systems.
MODULARITY
REScala

JEScala: Modular Coordination with Declarative Events and Joins

Jurgen M. Van Ham, Guido Salvaneschi, Mira Mezini, Jacques Noyé

In Proceedings of the 13th International Conference on Modularity, MODULARITY, 2014

Abstract PDF

Advanced concurrency abstractions overcome the drawbacks of low-level techniques such as locks and monitors, freeing programmers that implement concurrent applications from the burden of concentrating on low-level details. However, with current approaches the coordination logic involved in complex coordination schemas is fragmented into several pieces including join patterns, data emissions triggered in different places of the application, and the application logic that implicitly creates dependencies among communication channels, hence indirectly among join patterns. We present JEScala, a language that captures coordination schemas in a more expressive and modular way by leveraging a seamless integration of an advanced event system with join abstractions. We validate our approach with case studies and provide a first performance assessment.
MODULARITY
REScala

REScala: Bridging between Object-Oriented and Functional Style in Reactive Applications

Guido Salvaneschi, Gerold Hintz, Mira Mezini

In Proceedings of the 13th International Conference on Modularity, MODULARITY, 2014

Abstract PDF

Traditionally, object-oriented software adopts the Observer pattern to implement reactive behavior. Its drawbacks are well-documented and two families of alternative approaches have been proposed, extending object-oriented languages with concepts from functional reactive and dataflow programming, respectively event-driven programming. The former hardly escape the functional setting; the latter do not achieve the declarativeness of more functional approaches.
In this paper, we present REScala, a reactive language which integrates concepts from event-based and functional-reactive programming into the object-oriented world. REScala supports the development of reactive applications by fostering a functional declarative style which complements the advantages of object-oriented design.
LNCS
REScala

Towards Reactive Programming for Object-Oriented Applications

Guido Salvaneschi, Mira Mezini

In Transactions on Aspect-Oriented Software Development XI, Lecture Notes in Computer Science, 2014

Abstract PDF

Reactive applications are difficult to implement. Traditional solutions based on event systems and the Observer pattern have a number of inconveniences, but programmers bear them in return for the benefits of OO design. On the other hand, reactive approaches based on automatic updates of dependencies – like functional reactive programming and dataflow languages – provide undoubted advantages but do not fit well with mutable objects.
In this paper, we provide a research roadmap to overcome the limitations of the current approaches and to support reactive applications in the OO setting. To establish a solid background for our investigation, we propose a conceptual framework to model the design space of reactive applications and we study the flaws of the existing solutions. Then we highlight how reactive languages have the potential to address those issues and we formulate our research plan.

2013

REM
REScala

Ways to React: Comparing Reactive Languages and Complex Event

Alessandro Margara, Guido Salvaneschi

Presentation at the Workshop on Reactivity, Events and Modularity (REM), 2013

Abstract PDF

Reactive applications demand for detecting the changes that occur in a domain of interest and for timely reactions. Examples range from simple interactive applications to complex monitoring tasks involving distributed and heterogeneous systems.
Over the last years, different programming paradigms and solutions have been proposed to support such applications. In this paper, we focus on two prominent approaches: event-based programming, specifically Complex Event Processing (CEP), and Reactive Languages (RLs).
CEP systems enable the definition of high level situations of interest from low level primitive events detected in the external environment. On the other hand, RLs support time-changing values and their composition as dedicated language abstractions. These research fields have been investigated by different communities, belonging respectively to the database and the distributed systems areas and to the programming language area.
It is our belief that a deeper understanding of these research fields, including their benefits and limitations, their similarities and differences, could drive further developments in supporting reactive applications. For this reason, we propose a first comparison of the two fields. Despite huge differences, we believe that such a comparison can trigger an interesting discussion across the communities, favor knowledge sharing, and let new ideas emerge.
TAAS

An Analysis of Language-Level Support for Self-Adaptive Software

Guido Salvaneschi, Carlo Ghezzi, Matteo Pradella

ACM Transactions on Autonomous and Adaptive Systems 8 (2), 2013

Abstract PDF

Self-adaptive software has become increasingly important to address the new challenges of complex computing systems. To achieve adaptation, software must be designed and implemented by following suitable criteria, methods, and strategies. Past research has been mostly addressing adaptation by developing solutions at the software architecture level. This work, instead, focuses on finer-grain programming language-level solutions. We analyze three main linguistic approaches: metaprogramming, aspect-oriented programming, and context-oriented programming. The first two are general-purpose linguistic mechanisms, whereas the third is a specific and focused approach developed to support context-aware applications. This paradigm provides specialized language-level abstractions to implement dynamic adaptation and modularize behavioral variations in adaptive systems.
The article shows how the three approaches can support the implementation of adaptive systems and compares the pros and cons offered by each solution.
COORDINATION
REScala

Towards Distributed Reactive Programming

Guido Salvaneschi, Joscha Drechsler, Mira Mezini

In Proceedings of the International Conference on Coordination Languages and Models, COORDINATION, 2013

Abstract PDF

Reactive applications is a wide class of software that responds to user input, network messages, and other events. Recent research on reactive languages successfully addresses the drawbacks of the Observer pattern – the traditional way reactive applications are implemented in the object-oriented setting – by introducing time-changing values and other ad-hoc programming abstractions.
However, those approaches are limited to local settings, but most applications are distributed. We highlight the research challenges of distributed reactive programming and present a research roadmap. We argue that distributed reactive programming not only moves reactive languages to the distributed setting, but is a promising concept for middleware and distributed systems design.
AOSD
REScala

Reactive Behavior in Object-Oriented Applications: An Analysis and a Research Roadmap

Guido Salvaneschi, Mira Mezini

In Proceedings of the 12th Annual International Conference on Aspect-Oriented Software Development, AOSD, 2013

Abstract PDF

Reactive applications are difficult to implement. Traditional solutions based on event systems and the Observer pattern have a number of inconveniences, but programmers bear them in return for the benefits of OO design. On the other hand, reactive approaches based on automatic updates of dependencies - like functional reactive programming and dataflow languages - provide undoubted advantages but do not fit well with mutable objects.
In this paper, we provide a research roadmap to overcome the limitations of the current approaches and to support reactive applications in the OO setting. To establish a solid background for our investigation, we propose a conceptual framework to model the design space of reactive applications and we study the flaws of the existing solutions. Then we highlight how reactive languages have the potential to address those issues and we formulate our research plan.

2012

JSS

Context-Oriented Programming: A Software Engineering Perspective

Guido Salvaneschi, Carlo Ghezzi, Matteo Pradella

Journal of Systems and Software 85 (8), 2012

Abstract PDF

The implementation of context-aware systems can be supported through the adoption of techniques at the architectural level such as middlewares or component-oriented architectures. It can also be supported by suitable constructs at the programming language level. Context-oriented programming (COP) is emerging as a novel paradigm for the implementation of this kind of software, in particular in the field of mobile and ubiquitous computing. The COP paradigm tackles the issue of developing context-aware systems at the language-level, introducing ad hoc language abstractions to manage adaptations modularization and their dynamic activation. In this paper we review the state of the art in the field of COP in the perspective of the benefits that this technique can provide to software engineers in the design and implementation of context-aware applications.
AOSD

ContextErlang: Introducing Context-Oriented Programming in the Actor Model

Guido Salvaneschi, Carlo Ghezzi, Matteo Pradella

In Proceedings of the 11th Annual International Conference on Aspect-Oriented Software Development, AOSD, 2012

Abstract PDF

Self-adapting systems are becoming widespread in emerging fields such as autonomic, mobile and ubiquitous computing. Context-oriented programming (COP) is a promising language-level solution for the implementation of context-aware, self-adaptive software. However, current COP approaches struggle to effectively manage the asynchronous nature of context provisioning.
We argue that, to solve these issues, COP features should be designed to fit nicely in the concurrency model supported by the language. This work presents the design rationale of ContextErlang, which introduces COP in the Actor Model. We provide evidence that ContextErlang constitutes a viable solution to implement context-aware software in a highly concurrent and distributed setting. We discuss a case study and an evaluation of run-time performance.

2011

ICISS

Finding Non-Trivial Malware Naming Inconsistencies

Federico Maggi, Andrea Bellini, Guido Salvaneschi, Stefano Zanero

In Proceedings of the 7th International Conference on Information Systems Security, ICISS, 2011

Abstract PDF

Malware analysts, and in particular antivirus vendors, never agreed on a single naming convention for malware specimens. This leads to confusion and difficulty—more for researchers than for practitioners—for example, when comparing coverage of different antivirus engines, when integrating and systematizing known threats, or comparing the classifications given by different detectors. Clearly, solving naming inconsistencies is a very difficult task, as it requires that vendors agree on a unified naming convention. More importantly, solving inconsistencies is impossible without knowing exactly where they are. Therefore, in this paper we take a step back and concentrate on the problem of finding inconsistencies. To this end, we first represent each vendor’s naming convention with a graph-based model. Second, we give a precise definition of inconsistency with respect to these models. Third, we define two quantitative measures to calculate the overall degree of inconsistency between vendors. In addition, we propose a fast algorithm that finds non-trivial (i.e., beyond syntactic differences) inconsistencies. Our experiments on four major antivirus vendors and 98,798 real-world malware samples confirm anecdotal observations that different vendors name viruses differently. More importantly, we were able to find inconsistencies that cannot be inferred at all by looking solely at the syntax.
COP

JavaCtx: Seamless Toolchain Integration for Context-Oriented Programming

Guido Salvaneschi, Carlo Ghezzi, Matteo Pradella

In Proceedings of the 3rd International Workshop on Context-Oriented Programming, COP, 2011

Abstract PDF

Context-oriented programming is an emerging paradigm addressing at the language level the issue of dynamic software adaptation and modularization of context-specific concerns. In this paper we propose JavaCtx, a tool which employs coding conventions to generate the context-aware semantics for Java programs and subsequently weave it into the application. The contribution of JavaCtx is twofold: the design of a set of coding conventions which allow to write context-oriented software in plain Java and the concept of context-oriented semantics injection, which allows to introduce the context-aware semantics through standard aspect-oriented programming. Both of these points allow to seamless integrate JavaCtx in the existing industrial-strength appliances and so ease the development of context-oriented software in consolidated industrial settings.
SEAMS

An Evaluation of the Adaptation Capabilities in Programming Languages

Carlo Ghezzi, Matteo Pradella, Guido Salvaneschi

In Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS, 2011

Abstract PDF

In recent years the need for software applications to adapt to the environment in which they are situated has become common. Beside architectural approaches, language-level support for the development of adaptable and context-aware software have been investigated. Many existing solutions adopt ad hoc programming paradigms such as aspect oriented programming (AOP) or context oriented programming (COP). In this paper we investigate the use of the abstractions offered by traditional object-oriented and functional paradigms for the development of context-adaptable systems. We carry out our analysis along a set of conceptual directions which consider the requirement of functional adaptation beside non functional requirements such as safety and effective modularization. Our analysis were validated though the development of several prototypes of an adaptable cache server which is chosen as the running example through the paper. We provide an estimation of the performance advantages of the techniques based traditional programming languages compared with context-oriented programming.
CoRR

Context-Oriented Programming: A Programming Paradigm for Autonomic Systems

Guido Salvaneschi, Carlo Ghezzi, Matteo Pradella

arXiv, 2011

Abstract

Dynamic software adaptability is one of the central features leveraged by autonomic computing. However, developing software that changes its behavior at run time adapting to the operational conditions is a challenging task. Several approaches have been proposed in the literature to attack this problem at different and complementary abstraction levels: software architecture, middleware, and programming level. We focus on the support that ad-hoc programming language constructs may provide to support dynamically adaptive behaviors. We introduce context-oriented programming languages and we present a framework that positions the supported paradigm in the MAPE-K autonomic loop. We discuss the advantages of using context-oriented programming languages instead of other mainstream approaches based on dynamic aspect-oriented programming languages. We present a preliminary case study that shows how the proposed programming style naturally fits dynamic adaptation requirements and we extensively evaluate the use of COP in this scenario. Finally, we discuss some known problems and outline a number of open research challenges.
Metrics of Software Security

Guido Salvaneschi, Paolo Salvaneschi

In Encyclopedia of Cryptography and Security, 2nd Ed, 2011

Abstract

Measuring software security requires to identify measurable properties of a software artifact and to build models that can relate the measures to a qualitative or quantitative value of the property “security”.

2010

COP

Context Oriented Programming in Highly Concurrent Systems

Carlo Ghezzi, Matteo Pradella, Guido Salvaneschi

In Proceedings of the 2nd International Workshop on Context-Oriented Programming, COP, 2010

Abstract PDF

Context Oriented Programming (COP) allows modularization of programs according to the cross-cutting concern of contexts. Context depending features are grouped in layers which can be activated at run time by triggering the associated behavioral variations.
COP extensions have been provided for different languages. However all of them enforce a thread, shared-memory based concurrency model. In this paper we discuss how the COP paradigm can be applied to message-based concurrent systems which support the agents paradigm. The discussion is supported by the case of ContextErlang, our COP-inspired contextual version of Erlang.
SP

Identifying Dormant Functionality in Malware Programs

Paolo Milani Comparetti, Guido Salvaneschi, Engin Kirda, Clemens Kolbitsch, Christopher Kruegel, Stefano Zanero

In Proceedings of the 2010 IEEE Symposium on Security and Privacy, SP, 2010

Abstract PDF

To handle the growing flood of malware, security vendors and analysts rely on tools that automatically identify and analyze malicious code. Current systems for automated malware analysis typically follow a dynamic approach, executing an unknown program in a controlled environment (sandbox) and recording its runtime behavior. Since dynamic analysis platforms directly run malicious code, they are resilient to popular malware defense techniques such as packing and code obfuscation. Unfortunately, in many cases, only a small subset of all possible malicious behaviors is observed within the short time frame that a malware sample is executed. To mitigate this issue, previous work introduced techniques such as multi-path or forced execution to increase the coverage of dynamic malware analysis. Unfortunately, using these techniques is potentially expensive, as the number of paths that require analysis can grow exponentially.
In this paper, we propose Reanimator, a novel solution to determine the capabilities (malicious functionality) of malware programs. Our solution is based on the insight that we can leverage behavior observed while dynamically executing a specific malware sample to identify similar functionality in other programs. More precisely, when we observe malicious actions during dynamic analysis, we automatically extract and model the parts of the malware binary that are responsible for this behavior. We then leverage these models to check whether similar code is present in other samples. This allows us to statically identify dormant functionality (functionality that is not observed during dynamic analysis) in malicious programs. We evaluate our approach on thousands of real-world malware samples, and we show that our system is successful in identifying additional, malicious functionality. As a result, our approach can significantly improve the coverage of malware analysis results.
SEAMS

Programming Language Support to Context-Aware Adaptation: A Case-Study with Erlang

Carlo Ghezzi, Matteo Pradella, Guido Salvaneschi

In Proceedings of the 2010 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, SEAMS, 2010

Abstract PDF

Software applications are increasingly situated in a world where context changes continuously. At the same time, applications need to provide continuous service, and the service provided often needs to change in order to adapt to the new contexts. Context-aware adaptation can be greatly facilitated by using programming languages that natively support high-level features to deal with contexts, context changes, and context-aware behaviors. Although context-oriented programming has been around for a while, most existing efforts focus on incorporating context-oriented features in languages that are not primarily oriented to concurrency, distribution, and dynamic reconfiguration. These features, however, characterize most pervasive context-aware situations. In this work, we illustrate how context-aware programming primitives may introduced in the parallel and distributed Erlang programming language. We also present an extended example, which illustrates the benefits of using our extension (ContextErlang) to design context-aware pervasive applications.
FASE

Automatic Cross Validation of Multiple Specifications: A Case Study

Carlo Ghezzi, Andrea Mocci, Guido Salvaneschi

In Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering, FASE, 2010

Abstract

The problem of formal software specification has been addressed and discussed since the infancy of software engineering. However, among all the proposed solutions, none is universally accepted yet. Many different formal descriptions can in fact be given for the same software component; thus, the problem of determining the consistency relation among those descriptions becomes relevant and potentially critical. In this work, we propose a method for comparing two specific kinds of formal specifications of containers. In particular, we check the consistency of intensional behavior models with algebraic specifications. The consistency check is performed by generating a behavioral equivalence model from the intensional model, converting the algebraic axioms into temporal logic formulae, and then checking them against the model by using the NuSMV model checker. An automated software tool which encodes the problem as model checking has been implemented to check the consistency of recovered specifications of relevant Java classes.

2009

EC2ND

Integrated Detection of Attacks Against Browsers, Web Applications and Databases

Claudio Criscione, Guido Salvaneschi, Federico Maggi, Stefano Zanero

In Proceedings of the 2009 European Conference on Computer Network Defense, EC2ND, 2009

Abstract PDF

Anomaly-based techniques were exploited successfully to implement protection mechanisms for various systems. Recently, these approaches have been ported to the web domain under the name of "web application anomaly detectors" (or firewalls) with promising results. In particular, those capable of automatically building specifications, or models, of the protected application by observing its traffic (e.g., network packets, system calls, or HTTP requests and responses) are particularly interesting, since they can be deployed with little effort.
Typically, the detection accuracy of these systems is significantly influenced by the model building phase (often called training), which clearly depends upon the quality of the observed traffic, which should resemble the normal activity of the protected application and must be also free from attacks. Otherwise, detection may result in significant amounts of false positives (i.e., benign events flagged as anomalous) and negatives (i.e., undetected threats).
In this work we describe Masibty, a web application anomaly detector that have some interesting properties. First, it requires the training data not to be attack-free. Secondly, not only it protects the monitored application, it also detects and blocks malicious client-side threats before they are sent to the browser. Third, Masibty intercepts the queries before they are sent to the database, correlates them with the corresponding HTTP requests and blocks those deemed anomalous.
Both the accuracy and the performance have been evaluated on real-world web applications with interesting results. The system is almost not influenced by the presence of attacks in the training data and shows only a negligible amount of false positives, although this is paid in terms of a slight performance overhead.