Back to Events

Seminar Series

July 14

Flexible Information-Flow Control

Daniel Schoepe
Chalmers University of Technology

Part Of

2:00P
- 3:00P

Location

32-G449
Add to Calendar 2017-07-14 14:00:00 2017-07-14 15:00:00 America/New_York Flexible Information-Flow Control Due to the pervasiveness of untrusted code handling sensitiveinformation, information leaks in programs pose a high risk of unwanteddata disclosure. While information-flow control techniques providestrong guarantees, they are not widely used in practice. Conversely morelight-weight techniques such as taint tracking lack formal guaranteesand analysis.To address this, we investigate more permissive techniques with weakerguarantees: Taint tracking is widely used, but hard to capture formally.We present a formal security definition of the security property itenforces and explore a new enforcement method based on the facetedvalues technique. Additionally, we establish a connection between thesecurity notions of opacity and noninterference. To make fully-fledgedinformation-flow control easier to use, we present an approach tosecure database-backed applications using homogeneous meta-programmingto secure applications combining server-side code, client-side code, anddatabase interactions. 32-G449

July 05

Approximations for Reasoning about Floating-Point Arithmetic

Aleksandar Zeljic
Uppsala University

Part Of

11:00A
- 1:00P

Location

Seminar Room D463 (Star)
Add to Calendar 2017-07-05 11:00:00 2017-07-05 13:00:00 America/New_York Approximations for Reasoning about Floating-Point Arithmetic Abstract:Safety-critical systems, especially those found in avionics and automotive industries, rely on various forms of machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic, especially FPA, can exhibit subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. The price of failure of safety-critical systems can be unacceptably high, since they can cost human lives or huge amounts of money, timeand effort. To prevent such occurrences, we want to formally prove that systems satisfy certain safety properties, or otherwise discover cases when the properties are violated. To achieve this, ability to formally reason about machine arithmetic is required. The main difficulty existing approaches face is their lack of scalability with the increasing complexity of systems and their properties.We present a general approximation refinement framework which we apply to solve constraints over floating-point arithmetic. It is built around an existing decision procedure, e.g., bit-blasting. Rather than solving the original formula, it solves a sequence of approximations of the formula, until either a model is found or the formula is determined to be unsatisfiable. Usually these type of refinement schemes use over- and under-approximations, however they are very difficult to design for floating-point arithmetic. Instead, theframework allows use of non-conservative approximations. The presented framework is general and preserves soundness, completeness and termination of the underlying procedure. In the case of floating-point arithmetic, it improves the solving time and the number of instancesthat can be solved when compared to bit-blasting alone.Bio:Aleksandar Zeljic is a PhD student at Department of Information Technology at Uppsala Unversity, advised by Philipp Ruemmer and Christoph Wintersteiger. His research focuses on improving scalability of SMT-style reasoning about machine arithmetic, through use of approximations and abstractions. Seminar Room D463 (Star)

June 22

Approximations for Reasoning about Floating-Point Arithmetic

Aleksandar Zeljic
Uppsala Unversity

Part Of

11:00A
- 12:00P

Location

Seminar Room D463 (Star)
Add to Calendar 2017-06-22 11:00:00 2017-06-22 12:00:00 America/New_York Approximations for Reasoning about Floating-Point Arithmetic Abstract:Safety-critical systems, especially those found in avionics andautomotive industries, rely on various forms of machine arithmetic toperform their tasks: integer arithmetic, fixed-point arithmetic orfloating-point arithmetic (FPA). Machine arithmetic, especially FPA,can exhibit subtle differences in behavior compared to the idealmathematical arithmetic, due to fixed-size representation in memory.The price of failure of safety-critical systems can be unacceptablyhigh, since they can cost human lives or huge amounts of money, timeand effort. To prevent such occurrences, we want to formally provethat systems satisfy certain safety properties, or otherwise discovercases when the properties are violated. To achieve this, ability toformally reason about machine arithmetic is required. The maindifficulty existing approaches face is their lack of scalability withthe increasing complexity of systems and their properties.We present a general approximation refinement framework which we applyto solve constraints over floating-point arithmetic. It is builtaround an existing decision procedure, e.g., bit-blasting. Rather thansolving the original formula, it solves a sequence of approximationsof the formula, until either a model is found or the formula isdetermined to be unsatisfiable. Usually these type of refinementschemes use over- and under-approximations, however they are verydifficult to design for floating-point arithmetic. Instead, theframework allows use of non-conservative approximations. The presentedframework is general and preserves soundness, completeness andtermination of the underlying procedure. In the case of floating-pointarithmetic, it improves the solving time and the number of instancesthat can be solved when compared to bit-blasting alone.Bio:Aleksandar Zeljic is a PhD student at Department of InformationTechnology at Uppsala Unversity, advised by Philipp Ruemmer andChristoph Wintersteiger. His research focuses on improving scalability of SMT-style reasoning about machine arithmetic, through use of approximations and abstractions. Seminar Room D463 (Star)

May 01

Lightweight formal methods for LLVM verification

Santosh Nagarakatte
Rutgers

Part Of

4:00P
- 5:00P

Location

32-G882
Add to Calendar 2017-05-01 16:00:00 2017-05-01 17:00:00 America/New_York Lightweight formal methods for LLVM verification Abstract:Peephole optimizations perform local algebraic simplifications to improve the efficiency of the code input to the compiler. These optimizations are a persistent source of bugs. The talk will present domain specific languages (DSL) in the Alive-NJ tool kit to verify both integer and floating point based peephole optimizations in LLVM. The talk will briefly highlight the challenges in handling the ambiguities in the LLVM's semantics. A transformation expressed in these DSLs is shown to be correct by automatically encoding it as constraints whose validity is checked using a satisfiability modulo theory (SMT) solver. Furthermore, an optimization expressed in the DSL can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. The talk will also highlight our recent results and future directions on data driven precondition inference for these optimizations, which will be useful while debugging an incorrect optimization. I will conclude the talk by briefly describing other active projects on approximations with Hadoop/Spark frameworks and profiling task parallel programs.Speaker Bio:Santosh Nagarakatte is an Assistant Professor of Computer Science at Rutgers University. He obtained his PhD from the University of Pennsylvania in 2012. His research interests are in Hardware-Software Interfaces spanning Programming Languages, Compilers, Software Engineering, and Computer Architecture. His papers have been selected as IEEE MICRO TOP Picks papers of computer architecture conferences in 2010 and 2013. He has received the NSF CAREER Award in 2015, ACM SIGPLAN PLDI 2015 Distinguished Paper Award, and ACM SIGSOFT ICSE 2016 Distinguished Paper Award for his research on LLVM compiler verification. 32-G882