ASPLOS @ EPFL Special seminar bundle
Event details
| Date | 18.02.2014 |
| Hour | 13:15 › 16:00 |
| Speaker | Radu Banabic, Stefan Bucur, Stanko Novakovic |
| Location | |
| Category | Conferences - Seminars |
EPFL has three papers this year at ASPLOS, the premier interdisciplinary conference on Architectural Support for Programming Languages and Operating Systems. We will have a special seminar of back-to-back presentations at EPFL ahead of the conference.
There will be a break between the talks, so it is possible to join-in or leave in the middle.
1:15 Radu Banabic, George Candea, and Rachid Guerraoui.
Finding Trojan Message Vulnerabilities in Distributed Systems.
http://dslab.epfl.ch/pubs/Achilles.pdf
Trojan messages are messages that seem correct to the re- ceiver but cannot be generated by any correct sender. Such messages constitute major vulnerability points of a dis- tributed system—they constitute ideal targets for a malicious actor and facilitate failure propagation across nodes. We describe Achilles, a tool that searches for Trojan messages in a distributed system. Achilles uses dynamic white-box analysis on the distributed system binaries in order to infer the predicate that defines messages parsed by receiver nodes and generated by sender nodes, respectively, and then com- putes Trojan messages as the difference between the two.
We apply Achilles on implementations of real distributed systems: FSP, a file transfer application, and PBFT, a Byzantine-fault-tolerant state machine replication library. Achilles discovered a new bug in FSP and rediscovered a previously known vulnerability in PBFT. In our evaluation we demonstrate that our approach can perform orders of magnitude better than general approaches based on regular fuzzing and symbolic execution.
2:15 Stefan Bucur, Johannes Kinder, and George Candea.
Prototyping Symbolic Execution Engines for Interpreted Languages.
http://infoscience.epfl.ch/record/195687
Symbolic execution is being successfully used to automat- ically test statically compiled code [4, 7, 9, 15]. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.
We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called CHEF) for turning a vanilla interpreter into a sound and complete sym- bolic execution engine. CHEF symbolically executes the target program by symbolically executing the interpreter’s binary while exploiting inferred knowledge about the pro- gram’s high-level structure.
Using CHEF, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. CHEF-produced engines are up to 1000× more performant than if directly executing the interpreter symbolically without CHEF.
3:15 Stanko Novakovic; Alexandros Daglis; Edouard Bugnion; Babak Falsafi; Boris Grot.
Scale-Out NUMA
http://infoscience.epfl.ch/record/195238
Emerging datacenter applications operate on vast datasets that are kept in DRAM to minimize latency. The large number of servers needed to accommodate this massive memory footprint requires frequent server-to-server communication in applications such as key-value stores and graph-based applications that rely on large irregular data structures. The fine-grained nature of the accesses is a poor match to commodity networking technologies, including RDMA, which incur delays of 10-1000x over local DRAM operations. We introduce Scale-Out NUMA (soNUMA) – an architecture, programming model, and communication protocol for low-latency, distributed in-memory processing. soNUMA layers an RDMA-inspired programming model directly on top of a NUMA memory fabric via a stateless messaging protocol. To facilitate interactions between the application, OS, and the fabric, soNUMA relies on the remote memory controller – a new architecturally-exposed hardware block integrated into the node’s local coherence hierarchy. Our results based on cycle-accurate full-system simulation show that soNUMA performs remote reads at latencies that are within 4x of local DRAM, can fully utilize the available memory bandwidth, and can issue up to 10M remote memory operations per second per core.
There will be a break between the talks, so it is possible to join-in or leave in the middle.
1:15 Radu Banabic, George Candea, and Rachid Guerraoui.
Finding Trojan Message Vulnerabilities in Distributed Systems.
http://dslab.epfl.ch/pubs/Achilles.pdf
Trojan messages are messages that seem correct to the re- ceiver but cannot be generated by any correct sender. Such messages constitute major vulnerability points of a dis- tributed system—they constitute ideal targets for a malicious actor and facilitate failure propagation across nodes. We describe Achilles, a tool that searches for Trojan messages in a distributed system. Achilles uses dynamic white-box analysis on the distributed system binaries in order to infer the predicate that defines messages parsed by receiver nodes and generated by sender nodes, respectively, and then com- putes Trojan messages as the difference between the two.
We apply Achilles on implementations of real distributed systems: FSP, a file transfer application, and PBFT, a Byzantine-fault-tolerant state machine replication library. Achilles discovered a new bug in FSP and rediscovered a previously known vulnerability in PBFT. In our evaluation we demonstrate that our approach can perform orders of magnitude better than general approaches based on regular fuzzing and symbolic execution.
2:15 Stefan Bucur, Johannes Kinder, and George Candea.
Prototyping Symbolic Execution Engines for Interpreted Languages.
http://infoscience.epfl.ch/record/195687
Symbolic execution is being successfully used to automat- ically test statically compiled code [4, 7, 9, 15]. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.
We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called CHEF) for turning a vanilla interpreter into a sound and complete sym- bolic execution engine. CHEF symbolically executes the target program by symbolically executing the interpreter’s binary while exploiting inferred knowledge about the pro- gram’s high-level structure.
Using CHEF, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. CHEF-produced engines are up to 1000× more performant than if directly executing the interpreter symbolically without CHEF.
3:15 Stanko Novakovic; Alexandros Daglis; Edouard Bugnion; Babak Falsafi; Boris Grot.
Scale-Out NUMA
http://infoscience.epfl.ch/record/195238
Emerging datacenter applications operate on vast datasets that are kept in DRAM to minimize latency. The large number of servers needed to accommodate this massive memory footprint requires frequent server-to-server communication in applications such as key-value stores and graph-based applications that rely on large irregular data structures. The fine-grained nature of the accesses is a poor match to commodity networking technologies, including RDMA, which incur delays of 10-1000x over local DRAM operations. We introduce Scale-Out NUMA (soNUMA) – an architecture, programming model, and communication protocol for low-latency, distributed in-memory processing. soNUMA layers an RDMA-inspired programming model directly on top of a NUMA memory fabric via a stateless messaging protocol. To facilitate interactions between the application, OS, and the fabric, soNUMA relies on the remote memory controller – a new architecturally-exposed hardware block integrated into the node’s local coherence hierarchy. Our results based on cycle-accurate full-system simulation show that soNUMA performs remote reads at latencies that are within 4x of local DRAM, can fully utilize the available memory bandwidth, and can issue up to 10M remote memory operations per second per core.
Practical information
- Informed public
- Free
- This event is internal
Organizer
- Edouard Bugnion