-
BFTBrain: Adaptive BFT Consensus with Reinforcement Learning
Authors:
Chenyuan Wu,
Haoyun Qin,
Mohammad Javad Amiri,
Boon Thau Loo,
Dahlia Malkhi,
Ryan Marcus
Abstract:
This paper presents BFTBrain, a reinforcement learning (RL) based Byzantine fault-tolerant (BFT) system that provides significant operational benefits: a plug-and-play system suitable for a broad set of hardware and network configurations, and adjusts effectively in real-time to changing fault scenarios and workloads. BFTBrain adapts to system conditions and application needs by switching between…
▽ More
This paper presents BFTBrain, a reinforcement learning (RL) based Byzantine fault-tolerant (BFT) system that provides significant operational benefits: a plug-and-play system suitable for a broad set of hardware and network configurations, and adjusts effectively in real-time to changing fault scenarios and workloads. BFTBrain adapts to system conditions and application needs by switching between a set of BFT protocols in real-time. Two main advances contribute to BFTBrain's agility and performance. First, BFTBrain is based on a systematic, thorough modeling of metrics that correlate the performance of the studied BFT protocols with varying fault scenarios and workloads. These metrics are fed as features to BFTBrain's RL engine in order to choose the best-performing BFT protocols in real-time. Second, BFTBrain coordinates RL in a decentralized manner which is resilient to adversarial data pollution, where nodes share local metering values and reach the same learning output by consensus. As a result, in addition to providing significant operational benefits, BFTBrain improves throughput over fixed protocols by $18\%$ to $119\%$ under dynamic conditions and outperforms state-of-the-art learning based approaches by $44\%$ to $154\%$.
△ Less
Submitted 12 August, 2024;
originally announced August 2024.
-
Safety Verification of Declarative Smart Contracts
Authors:
Haoxian Chen,
Lan Lu,
Brendan Massey,
Yuepeng Wang,
Boon Thau Loo
Abstract:
Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementa…
▽ More
Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
△ Less
Submitted 2 August, 2023; v1 submitted 26 November, 2022;
originally announced November 2022.
-
AdaChain: A Learned Adaptive Blockchain
Authors:
Chenyuan Wu,
Bhavana Mehta,
Mohammad Javad Amiri,
Ryan Marcus,
Boon Thau Loo
Abstract:
This paper presents AdaChain, a learning-based blockchain framework that adaptively chooses the best permissioned blockchain architecture in order to optimize effective throughput for dynamic transaction workloads. AdaChain addresses the challenge in the Blockchain-as-a-Service (BaaS) environments, where a large variety of possible smart contracts are deployed with different workload characteristi…
▽ More
This paper presents AdaChain, a learning-based blockchain framework that adaptively chooses the best permissioned blockchain architecture in order to optimize effective throughput for dynamic transaction workloads. AdaChain addresses the challenge in the Blockchain-as-a-Service (BaaS) environments, where a large variety of possible smart contracts are deployed with different workload characteristics. AdaChain supports automatically adapting to an underlying, dynamically changing workload through the use of reinforcement learning. When a promising architecture is identified, AdaChain switches from the current architecture to the promising one at runtime in a way that respects correctness and security concerns. Experimentally, we show that AdaChain can converge quickly to optimal architectures under changing workloads, significantly outperform fixed architectures in terms of the number of successfully committed transactions, all while incurring low additional overhead.
△ Less
Submitted 17 July, 2023; v1 submitted 3 November, 2022;
originally announced November 2022.
-
Declarative Smart Contracts
Authors:
Haoxian Chen,
Gerald Whitters,
Mohammad Javad Amiri,
Yuepeng Wang,
Boon Thau Loo
Abstract:
This paper presents DeCon, a declarative programming language for implementing smart contracts and specifying contract-level properties. Driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints, DeCon models each smart contract as a set of relational tables that store transaction records. This relational representat…
▽ More
This paper presents DeCon, a declarative programming language for implementing smart contracts and specifying contract-level properties. Driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints, DeCon models each smart contract as a set of relational tables that store transaction records. This relational representation of smart contracts enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance. Specifically, a DeCon program consists of a set of declarative rules and violation query rules over the relational representation, describing the smart contract implementation and contract-level properties, respectively. We have developed a tool that can compile DeCon programs into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. Our evaluation results reveal the marginal overhead of DeCon compared to the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.
△ Less
Submitted 27 July, 2022;
originally announced July 2022.
-
Templating Shuffles
Authors:
Qizhen Zhang,
Jiacheng Wu,
Ang Chen,
Vincent Liu,
Boon Thau Loo
Abstract:
Cloud data centers are evolving fast. At the same time, today's large-scale data analytics applications require non-trivial performance tuning that is often specific to the applications, workloads, and data center infrastructure. We propose TeShu, which makes network shuffling an extensible unified service layer common to all data analytics. Since an optimal shuffle depends on a myriad of factors,…
▽ More
Cloud data centers are evolving fast. At the same time, today's large-scale data analytics applications require non-trivial performance tuning that is often specific to the applications, workloads, and data center infrastructure. We propose TeShu, which makes network shuffling an extensible unified service layer common to all data analytics. Since an optimal shuffle depends on a myriad of factors, TeShu introduces parameterized shuffle templates, instantiated by accurate and efficient sampling that enables TeShu to dynamically adapt to different application workloads and data center layouts. Our preliminary experimental results show that TeShu efficiently enables shuffling optimizations that improve performance and adapt to a variety of data center network scenarios.
△ Less
Submitted 10 January, 2023; v1 submitted 21 July, 2022;
originally announced July 2022.
-
The Bedrock of Byzantine Fault Tolerance: A Unified Platform for BFT Protocol Design and Implementation
Authors:
Mohammad Javad Amiri,
Chenyuan Wu,
Divyakant Agrawal,
Amr El Abbadi,
Boon Thau Loo,
Mohammad Sadoghi
Abstract:
Byzantine Fault-Tolerant (BFT) protocols have recently been extensively used by decentralized data management systems with non-trustworthy infrastructures, e.g., permissioned blockchains. BFT protocols cover a broad spectrum of design dimensions from infrastructure settings such as the communication topology, to more technical features such as commitment strategy and even fundamental social choice…
▽ More
Byzantine Fault-Tolerant (BFT) protocols have recently been extensively used by decentralized data management systems with non-trustworthy infrastructures, e.g., permissioned blockchains. BFT protocols cover a broad spectrum of design dimensions from infrastructure settings such as the communication topology, to more technical features such as commitment strategy and even fundamental social choice properties like order-fairness. The proliferation of different BFT protocols has rendered it difficult to navigate the BFT landscape, let alone determine the protocol that best meets application needs. This paper presents Bedrock, a unified platform for BFT protocols design, analysis, implementation, and experiments. Bedrock proposes a design space consisting of a set of design choices capturing the trade-offs between different design space dimensions and providing fundamentally new insights into the strengths and weaknesses of BFT protocols. Bedrock enables users to analyze and experiment with BFT protocols within the space of plausible choices, evolve current protocols to design new ones, and even uncover previously unknown protocols. Our experimental results demonstrate the capability of Bedrock to uniformly evaluate BFT protocols in new ways that were not possible before due to the diverse assumptions made by these protocols. The results validate Bedrock's ability to analyze and derive BFT protocols.
△ Less
Submitted 3 August, 2022; v1 submitted 9 May, 2022;
originally announced May 2022.
-
NetRep: Automatic Repair for Network Programs
Authors:
Lei Shi,
Yuepeng Wang,
Rajeev Alur,
Boon Thau Loo
Abstract:
Debugging imperative network programs is a challenging task for developers because understanding various network modules and complicated data structures is typically time-consuming. To address the challenge, this paper presents an automated technique for repairing network programs from unit tests. Specifically, given as input a faulty network program and a set of unit tests, our approach localizes…
▽ More
Debugging imperative network programs is a challenging task for developers because understanding various network modules and complicated data structures is typically time-consuming. To address the challenge, this paper presents an automated technique for repairing network programs from unit tests. Specifically, given as input a faulty network program and a set of unit tests, our approach localizes the fault through symbolic reasoning, and synthesizes a patch such that the repaired program can pass all unit tests. It applies domain-specific abstraction to simplify network data structures and utilizes modular analysis to facilitate function summary reuse for symbolic analysis. We implement the proposed techniques in a tool called NetRep and evaluate it on 10 benchmarks adapted from real-world software-defined networking controllers. The evaluation results demonstrate the effectiveness and efficiency of NetRep for repairing network programs.
△ Less
Submitted 20 October, 2021; v1 submitted 12 October, 2021;
originally announced October 2021.
-
Qanaat: A Scalable Multi-Enterprise Permissioned Blockchain System with Confidentiality Guarantees
Authors:
Mohammad Javad Amiri,
Boon Thau Loo,
Divyakant Agrawal,
Amr El Abbadi
Abstract:
Today's large-scale data management systems need to address distributed applications' confidentiality and scalability requirements among a set of collaborative enterprises. This paper presents Qanaat, a scalable multi-enterprise permissioned blockchain system that guarantees the confidentiality of enterprises in collaboration workflows. Qanaat presents data collections that enable any subset of en…
▽ More
Today's large-scale data management systems need to address distributed applications' confidentiality and scalability requirements among a set of collaborative enterprises. This paper presents Qanaat, a scalable multi-enterprise permissioned blockchain system that guarantees the confidentiality of enterprises in collaboration workflows. Qanaat presents data collections that enable any subset of enterprises involved in a collaboration workflow to keep their collaboration private from other enterprises. A transaction ordering scheme is also presented to enforce only the necessary and sufficient constraints on transaction order to guarantee data consistency. Furthermore, Qanaat supports data consistency across collaboration workflows where an enterprise can participate in different collaboration workflows with different sets of enterprises. Finally, Qanaat presents a suite of consensus protocols to support intra-shard and cross-shard transactions within or across enterprises.
△ Less
Submitted 17 July, 2022; v1 submitted 22 July, 2021;
originally announced July 2021.
-
Saguaro: An Edge Computing-Enabled Hierarchical Permissioned Blockchain
Authors:
Mohammad Javad Amiri,
Ziliang Lai,
Liana Patel,
Boon Thau Loo,
Eric Lo,
Wenchao Zhou
Abstract:
We present Saguaro, a permissioned blockchain system designed specifically for edge computing networks. Saguaro leverages the hierarchical structure of edge computing networks to reduce the overhead of wide-area communication by presenting several techniques. First, Saguaro proposes coordinator-based and optimistic protocols to process cross-domain transactions with low latency where the lowest co…
▽ More
We present Saguaro, a permissioned blockchain system designed specifically for edge computing networks. Saguaro leverages the hierarchical structure of edge computing networks to reduce the overhead of wide-area communication by presenting several techniques. First, Saguaro proposes coordinator-based and optimistic protocols to process cross-domain transactions with low latency where the lowest common ancestor of the involved domains coordinates the protocol or detects inconsistency. Second, data are collected over hierarchy enabling higher-level domains to aggregate their sub-domain data. Finally, transactions initiated by mobile edge devices are processed without relying on high-level fog and cloud servers. Our experimental results across a wide range of workloads demonstrate the scalability of Saguaro in supporting a range of cross-domain and mobile transactions.
△ Less
Submitted 14 September, 2022; v1 submitted 21 January, 2021;
originally announced January 2021.
-
Session-layer Attack Traffic Classification by Program Synthesis
Authors:
Lei Shi,
Yahui Li,
Rajeev Alur,
Boon Thau Loo
Abstract:
Writing classification rules to identify malicious network traffic is a time-consuming and error-prone task. Learning-based classification systems automatically extract such rules from positive and negative traffic examples. However, due to limitations in the representation of network traffic and the learning strategy, these systems lack both expressiveness to cover a range of attacks and interpre…
▽ More
Writing classification rules to identify malicious network traffic is a time-consuming and error-prone task. Learning-based classification systems automatically extract such rules from positive and negative traffic examples. However, due to limitations in the representation of network traffic and the learning strategy, these systems lack both expressiveness to cover a range of attacks and interpretability in fully describing the attack traffic's structure at the session layer. This paper presents Sharingan system, which uses program synthesis techniques to generate network classification programs at the session layer. Sharingan accepts raw network traces as inputs, and reports potential patterns of the attack traffic in NetQRE, a domain specific language designed for specifying session-layer quantitative properties. Using Sharingan, network operators can better analyze the attack pattern due to the following advantages of Sharingan's learning process: (1) it requires minimal feature engineering, (2) it is amenable to efficient implementation of the learnt classifier, and (3) the synthesized program is easy to decipher and edit. We develop a range of novel optimizations that reduce the synthesis time for large and complex tasks to a matter of minutes. Our experiments show that Sharingan is able to correctly identify attacks from a diverse set of network attack traces and generates explainable outputs, while achieving accuracy comparable to state-of-the-art learning-based intrusion detection systems.
△ Less
Submitted 12 October, 2020;
originally announced October 2020.
-
RapidLearn: A General Purpose Toolkit for Autonomic Networking
Authors:
Jatin Sharma,
Nikhilesh Behera,
Priya Venkatraman,
Boon Thau Loo
Abstract:
Software Defined Networking has unfolded a new area of opportunity in distributed networking and intelligent networks. There has been a great interest in performing machine learning in distributed setting, exploiting the abstraction of SDN which makes it easier to write complex ML queries on standard control plane. However, most of the research has been made towards specialized problems (security,…
▽ More
Software Defined Networking has unfolded a new area of opportunity in distributed networking and intelligent networks. There has been a great interest in performing machine learning in distributed setting, exploiting the abstraction of SDN which makes it easier to write complex ML queries on standard control plane. However, most of the research has been made towards specialized problems (security, performance improvement, middlebox management etc) and not towards a generic framework. Also, existing tools and software require specialized knowledge of the algorithm/network to operate or monitor these systems. We built a generic toolkit which abstracts out the underlying structure, algorithms and other intricacies and gives an intuitive way for a common user to create and deploy distributed machine learning network applications. Decisions are made at local level by the switches and communicated to other switches to improve upon these decisions. Finally, a global decision is taken by controller based on another algorithm (in our case voting). We demonstrate efficacy of the framework through a simple DDoS detection algorithm.
△ Less
Submitted 9 September, 2020;
originally announced September 2020.
-
Sunstar: A Cost-effective Multi-Server Solution for Reliable Video Delivery
Authors:
Behnaz Arzani,
Nicholas Iodice,
Steven Hwang,
Prahalad Venkataramanan,
Roch Geurin,
Boon Thau Loo
Abstract:
In spite of much progress and many advances, cost-effective, high-quality video delivery over the internet remains elusive. To address this ongoing challenge, we propose Sunstar, a solution that leverages simultaneous downloads from multiple servers to preserve video quality. The novelty in Sunstar is not so much in its use of multiple servers but in the design of a schedule that balances improvem…
▽ More
In spite of much progress and many advances, cost-effective, high-quality video delivery over the internet remains elusive. To address this ongoing challenge, we propose Sunstar, a solution that leverages simultaneous downloads from multiple servers to preserve video quality. The novelty in Sunstar is not so much in its use of multiple servers but in the design of a schedule that balances improvements in video quality against increases in (peering) costs. The paper's main contributions are in elucidating the impact on the cost of various approaches towards improving video quality, including the use of multiple servers, and incorporating this understanding into the design of a scheduler capable of realizing an efficient trade-off. Our results show that Sunstar's scheduling algorithm can significantly improve performance (up to 50% in some instances) without cost impacts.
△ Less
Submitted 30 November, 2018;
originally announced December 2018.
-
007: Democratically Finding The Cause of Packet Drops
Authors:
Behnaz Arzani,
Selim Ciraci,
Luiz Chamon,
Yibo Zhu,
Hingqiang Liu,
Jitu Padhye,
Boon Thau Loo,
Geoff Outhred
Abstract:
Network failures continue to plague datacenter operators as their symptoms may not have direct correlation with where or why they occur. We introduce 007, a lightweight, always-on diagnosis application that can find problematic links and also pinpoint problems for each TCP connection. 007 is completely contained within the end host. During its two month deployment in a tier-1 datacenter, it detect…
▽ More
Network failures continue to plague datacenter operators as their symptoms may not have direct correlation with where or why they occur. We introduce 007, a lightweight, always-on diagnosis application that can find problematic links and also pinpoint problems for each TCP connection. 007 is completely contained within the end host. During its two month deployment in a tier-1 datacenter, it detected every problem found by previously deployed monitoring tools while also finding the sources of other problems previously undetected.
△ Less
Submitted 20 February, 2018;
originally announced February 2018.
-
FixRoute: A Unified Logic and Numerical Tool for Provably Safe Internet Traffic Engineering
Authors:
Behnaz Arzani,
Alexander Gurney,
Bo Li,
Xianglong Han,
Roch Guerin,
Boon Thau Loo
Abstract:
The performance of networks that use the Internet Protocol is sensitive to precise configuration of many low-level parameters on each network device. These settings govern the action of dynamic routing protocols, which direct the flow of traffic; in order to ensure that these dynamic protocols all converge to produce some 'optimal' flow, each parameter must be set correctly. Multiple conflicting o…
▽ More
The performance of networks that use the Internet Protocol is sensitive to precise configuration of many low-level parameters on each network device. These settings govern the action of dynamic routing protocols, which direct the flow of traffic; in order to ensure that these dynamic protocols all converge to produce some 'optimal' flow, each parameter must be set correctly. Multiple conflicting optimization objectives, nondeterminism, and the need to reason about different failure scenarios make the task particularly complicated.
We present a fast and flexible approach for the analysis of a number of such management tasks presented in the context of BGP routing. The idea is to combine {\em logical} satisfiability criteria with traditional {\em numerical} optimization, to reach a desired traffic flow outcome subject to given constraints on the routing process. The method can then be used to probe parameter sensitivity, trade-offs in the selection of optimization goals, resilience to failure, and so forth. The theory is underpinned by a rigorous abstraction of the convergence of distributed asynchronous message-passing protocols, and is therefore generalizable to other scenarios. Our resulting hybrid engine is faster than either purely logical or purely numeric alternatives, making it potentially feasible for interactive production use.
△ Less
Submitted 27 November, 2015;
originally announced November 2015.
-
A Program Logic for Verifying Secure Routing Protocols
Authors:
Chen Chen,
Limin Jia,
Hao Xu,
Cheng Luo,
Wenchao Zhou,
Boon Thau Loo
Abstract:
The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In this paper, we develop a sound program logic for SANDLog-a declarative specification language for secure routing protocols for verifying properties of these protoco…
▽ More
The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In this paper, we develop a sound program logic for SANDLog-a declarative specification language for secure routing protocols for verifying properties of these protocols. We prove invariant properties of SANDLog programs that run in an adversarial environment. As a step towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof obligations. VCGen is integrated into a compiler for SANDLog that can generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols can be carried out in this unified framework. To validate our framework, we encoded several proposed secure routing mechanisms in SANDLog, verified variants of path authenticity properties by manually discharging the generated verification conditions in Coq, and generated executable code based on SANDLog specification and ran the code in simulation.
△ Less
Submitted 27 December, 2015; v1 submitted 13 October, 2015;
originally announced October 2015.
-
Enabling Incremental Query Re-Optimization
Authors:
Mengmeng Liu,
Zachary G. Ives,
Boon Thau Loo
Abstract:
As declarative query processing techniques expand in scope --- to the Web, data streams, network routers, and cloud platforms --- there is an increasing need for adaptive query processing techniques that can re-plan in the presence of failures or unanticipated performance changes. A status update on the data distributions or the compute nodes may have significant repercussions on the choice of whi…
▽ More
As declarative query processing techniques expand in scope --- to the Web, data streams, network routers, and cloud platforms --- there is an increasing need for adaptive query processing techniques that can re-plan in the presence of failures or unanticipated performance changes. A status update on the data distributions or the compute nodes may have significant repercussions on the choice of which query plan should be running. Ideally, new system architectures would be able to make cost-based decisions about reallocating work, migrating data, etc., and react quickly as real-time status information becomes available. Existing cost-based query optimizers are not incremental in nature, and must be run "from scratch" upon each status or cost update. Hence, they generally result in adaptive schemes that can only react slowly to updates.
An open question has been whether it is possible to build a cost-based re-optimization architecture for adaptive query processing in a streaming or repeated query execution environment, e.g., by incrementally updating optimizer state given new cost information. We show that this can be achieved beneficially, especially for stream processing workloads. Our techniques build upon the recently proposed approach of formulating query plan enumeration as a set of recursive datalog queries; we develop a variety of novel optimization approaches to ensure effective pruning in both static and incremental cases. We implement our solution within an existing research query processing system, and show that it effectively supports cost-based initial optimization as well as frequent adaptivity.
△ Less
Submitted 22 September, 2014;
originally announced September 2014.
-
Measurements of Fission Products from the Fukushima Daiichi Incident in San Francisco Bay Area Air Filters, Automobile Filters, Rainwater, and Food
Authors:
A. R. Smith,
K. J. Thomas,
E. B. Norman,
D. L. Hurley,
B. T. Lo,
Y. D. Chan,
P. V. Guillaumon,
B. G. Harvey
Abstract:
A variety of environmental media were analyzed for fallout radionuclides resulting from the Fukushima nuclear accident by the Low Background Facility (LBF) at the Lawrence Berkeley National Laboratory (LBNL) in Berkeley, CA. Monitoring activities in air and rainwater began soon after the onset of the March 11, 2011 tsunami and are reported here through the end of 2012. Observed fallout isotopes in…
▽ More
A variety of environmental media were analyzed for fallout radionuclides resulting from the Fukushima nuclear accident by the Low Background Facility (LBF) at the Lawrence Berkeley National Laboratory (LBNL) in Berkeley, CA. Monitoring activities in air and rainwater began soon after the onset of the March 11, 2011 tsunami and are reported here through the end of 2012. Observed fallout isotopes include $^{131}$I, $^{132}$I,$^{132}$Te,$^{134}$Cs, $^{136}$Cs, and $^{137}$Cs. Isotopes were measured on environmental air filters, automobile filters, and in rainwater. An additional analysis of rainwater in search of $^{90}$Sr is also presented. Last, a series of food measurements conducted in September of 2013 are included due to extended media concerns of $^{134, 137}$Cs in fish. Similar measurements of fallout from the Chernobyl disaster at LBNL, previously unpublished publicly, are also presented here as a comparison with the Fukushima incident. All measurements presented also include natural radionuclides found in the environment to provide a basis for comparison.
△ Less
Submitted 27 December, 2013;
originally announced December 2013.
-
Cologne: A Declarative Distributed Constraint Optimization Platform
Authors:
Changbin Liu,
Lu Ren,
Boon Thau Loo,
Yun Mao,
Prithwish Basu
Abstract:
This paper presents Cologne, a declarative optimization platform that enables constraint optimization problems (COPs) to be declaratively specified and incrementally executed in distributed systems. Cologne integrates a declarative networking engine with an off-the-shelf constraint solver. We have developed the Colog language that combines distributed Datalog used in declarative networking with la…
▽ More
This paper presents Cologne, a declarative optimization platform that enables constraint optimization problems (COPs) to be declaratively specified and incrementally executed in distributed systems. Cologne integrates a declarative networking engine with an off-the-shelf constraint solver. We have developed the Colog language that combines distributed Datalog used in declarative networking with language constructs for specifying goals and constraints used in COPs. Cologne uses novel query processing strategies for processing Colog programs, by combining the use of bottom-up distributed Datalog evaluation with top-down goal-oriented constraint solving. Using case studies based on cloud and wireless network optimizations, we demonstrate that Cologne (1) can flexibly support a wide range of policy-based optimizations in distributed systems, (2) results in orders of magnitude less code compared to imperative implementations, and (3) is highly efficient with low overhead and fast convergence times.
△ Less
Submitted 26 April, 2012;
originally announced April 2012.
-
Declarative Reconfigurable Trust Management
Authors:
William Marczak,
David Zook,
Wenchao Zhou,
Molham Aref,
Boon Thau Loo
Abstract:
In recent years, there has been a proliferation of declarative logic-based trust management languages and systems proposed to ease the description, configuration, and enforcement of security policies. These systems have different tradeoffs in expressiveness and complexity, depending on the security constructs (e.g. authentication, delegation, secrecy, etc.) that are supported, and the assumed tr…
▽ More
In recent years, there has been a proliferation of declarative logic-based trust management languages and systems proposed to ease the description, configuration, and enforcement of security policies. These systems have different tradeoffs in expressiveness and complexity, depending on the security constructs (e.g. authentication, delegation, secrecy, etc.) that are supported, and the assumed trust level and scale of the execution environment. In this paper, we present LBTrust, a unified declarative system for reconfigurable trust management, where various security constructs can be customized and composed in a declarative fashion. We present an initial proof-of-concept implementation of LBTrust using LogicBlox, an emerging commercial Datalog-based platform for enterprise software systems. The LogicBlox language enhances Datalog in a variety of ways, including constraints and meta-programming, as well as support for programmer defined constraints which on the meta-model itself ? meta-constraints ? which act to restrict the set of allowable programs. LBTrust utilizes LogicBlox?s meta-programming and meta-constraints to enable customizable cryptographic, partitioning and distribution strategies based on the execution environment. We present uses cases of LBTrust based on three trust management systems (Binder, D1LP, and Secure Network Datalog), and provide a preliminary evaluation of a Binder-based trust management system.
△ Less
Submitted 9 September, 2009;
originally announced September 2009.