VERification, TEsting, Concurrency, Security / Semantics (VERTECS2) is a research group in the Department of Computer Science and Engineering at Indian Institute of Technology Delhi. We work in the areas of formal verification, concurrency, programming languages and security. Our group currently has three core faculty researchers and four Ph.D. students.
|Topic||Schedule||Discussion Lead||References/ Annotated Notes|
|Linear Temporal Logic||13-Apr-2017||Divyanshu||Principles of Model Checking (Chapter 5)|
|NetKAT||TBA||Arun Shankar||A Formal System for the Verification of Networks|
|Dependent Types in Databases||TBA||Chandrika|
|Compactness theorem - Lindstorm theorem||TBA||Divyanshu|
|Martin-Lof Type Theory||TBA||Chandrika|
|Regular Properties||Mar-2017||Divyanshu||Principles of Model Checking (Chapter 4)|
|Linear Time Properties||Feb-2017||Sanjana||Principles of Model Checking (Chapter 3)|
|Modeling Concurrent Systems||Jan-2017||Sanjana||Principles of Model Checking (Chapter 2)|
|Co-induction & Co-algebra||Sept-Dec-2016||Divyanshu||Universal Colgebra|
|Partial Order Reduction||26-May-2016||Chinmay||
|A Decentralized Model for Information Flow Control.||4-July-2015||Chandrika||Paper|
|Certification of programs for secure information flow.||26-June-2015||Chandrika||Paper|
|A Lattice Model of Secure Information Flow.||19-June-2015||Chandrika||Paper|
|Succinct Representation of Concurrent Trace Sets||22-May-2015||Dr Subodh Sharma|
|Nominal Modal Logic||Covered||Divyanshu|
|Testing Equivalences||Covered||Divyanshu||Observation Equivalences as Testing Equivalences|
|KAT||Covered||Prof. S. Arun Kumar|
|17/08/2016||Prof. Sorav Bansal||Program Synthesis from Polymorphic Refinement Types||We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a poly-morphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification and hence
synthesis of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a new algorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.
|24/08/2016||Prof. Subodh Sharma||Statistical Similarity of Binaries||We address the problem of finding similar procedures in stripped binaries. We present a new statistical approach for measuring the similarity between two procedures. Our notion of similarity allows us to find similar code even when it has been compiled using different compilers, or has been modified. The main idea is to use similarity by composition:
decompose the code into smaller comparable fragments, de-fine semantic similarity between fragments, and use statistical reasoning to lift fragment similarity into similarity between procedures. We have implemented our approach in a tool called Esh, and applied it to find various prominent vulnerabilities across compilers and versions, including Heartbleed , Shellshock  and Venom . We show that Esh produces high accuracy results, with few to no false positives a crucial factor in the scenario of vulnerability search in stripped binaries.
|31/08/2016||Deepak Ravi||Liquid Types||We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of
manual annotation. We have implemented liquid type inference in DSOLVE, which takes as input an OCAML program and a set of logical qualifiers and infers dependent types for the expressions in the OCAML program. To demonstrate the utility of our approach, we describe experiments using DSOLVE to statically verify the safety of array accesses on a set of OCAML benchmarks that were previously annotated with dependent types as part of the DML project. We show that when used in conjunction with a fixed set of array bounds checking qualifiers, DSOLVE reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%.
|07/09/2016||Manjeet Dahiya||Types from Data: Making Structured Data First-Class Citizens in F#||Most modern applications interact with external services and access data in structured formats such as XML, JSON and CSV. Static type systems do not understand such formats, often making data access more cumbersome. Should we give up and leave the messy world of external data to dynamic typing and runtime checks? Of course, not! We present F# Data, a library that integrates external structured data into F#. As most real-world data does not
come with an explicit schema, we develop a shape inference algorithm that infers a shape from representative sample documents. We then integrate the inferred shape into the F# type system using type providers. We formalize the process
and prove a relative type soundness theorem. Our library significantly reduces the amount of data access code and it provides additional safety guarantees when contrasted with the widely used weakly typed techniques.