Safe, Secure and Smart Software (S3) Lab


 
  Mission
 
Our research interests span the areas of formal methods and concurrent and distributed computing. We develop specification, verification and synthesis techniques and tools to build reliable, secure and efficient computing systems, in particular, subtle concurrent and distributed systems. We often reduce verification and synthesis to simple sufficient conditions to leverage the increasingly powerful automated and semi-automated reasoning techniques and tools.

Our research has been recognized as SIGPLAN Research Highlight in 2019 and received the distinguished paper award at OOPSLA'18 and ISSRE'15.

Prospective Students

 
  People


Farzin Hooshmand
Xiao Li
Paranshu Singhal

Graduated students:
   Jeremiah Griffin (undergraduate)
   Xiao Li (masters)

PI:
   Mohsen Lesani



  Recent Publications


Cross-Chain Transactions
Narges Shadab, Farzin Houshmand, Mohsen Lesani
ICBC'20 (IEEE International Conference on Blockchain and Cryptocurrency)

Polynomial-time Fence Insertion For Structured Programs
Mohammad Taheri, Arash Pourdamghani, Mohsen Lesani
DISC'19 (The International Symposium on Distributed Computing)
More

Replication Coordination Analysis and Synthesis
Farzin Hooshmand, Mohsen Lesani
Accepted with revisions to POPL'19 (ACM Principles of Programming Languages)
More

Transaction Protocol Verification with Labeled Synchronization Logic
Mohsen Lesani
NFM'19 (NASA Formal Methods Symposium)
More

BioScript: Programming Safe Chemistry of Laboratories-on-a-Chip
Jason Ott, Chris Curtis, Tyson Loveless, Mohsen Lesani, Philip Brisk
OOPSLA'18 (ACM Object-oriented Programming, Systems, Languages, and Applications)
Distinguished paper award
ACM SIGPLAN highlight
Invitied to Communications of ACM
More

The rest of publications


  Projects


Distributed Systems

Replication Coordination Analysis and Synthesis
Replicated systems are widely deployed to tolerate faults in aviation control systems and geo-distributed data stores. Given high-level sequential specifications, we automatically analyze the specifications and synthesize consistent, convergent and coordination-avoiding replicated distributed systems.
See the POPL'19 paper.

Certified Key-value Stores
We implement, specify and mechanically verify distributed key-value stores in proof assistants.
See the POPL'16 paper.

Ongoing project: Compositional Verification of Distributed System Stacks
What are the fundamental principles for compositional verification of distributed systems? We design program logics and compositional verification techniques to build certified distributed system stacks.
See our NSF-supported project.

Ongoing project: Automatic Synthesis of Parallel and Distributed Graph-processing Programs
Given a high-level specification of a graph processing problem, we automatically synthesize programs for multiple parallel and distributed graph-processing frameworks.

Blockchains and Cryptocurrencies

Cryptocurrency Exchange
How can we atomically exchange assets across multiple blockchains?
See the ICBC'20 paper.

Ongoing project: Certified Blockchains with Explicit Safety and Security Guarantees
What are the correctness conditions and verification principles for blockchain protocols? We aim at building certified blockchains with explicit safety and security guarantees using proof assistants.

Concurrent Systems

Transaction Specification, Testing and Verification
What are the correctness criteria and proof techniques for transactions?
See the DISC'14 paper, WTTM'12 and WTTM'13 papers.
We presented a testing technique that found bugs in transaction algorithms.
See the DISC'13 paper.
We have built a mechanically checked framework for verification of transactional memory algorithms.
See the CONCUR'12 paper.
We specify and implement safe transactions in the presence of communication between them.
See the PPoPP'12 paper.

Verification of Concurrent Data Structures
Composing atomic concurrent operations is challenging and researchers have found a myriad of atomicity bugs in compositions of concurrent libraries. We automatically verify the atomicity of compositions.
See the CAV'14 paper.

Automatic Fence Insertion
To gain performance, compilers and processors reorder program instructions. Reordering instructions may violate safety of concurrent executions. Experts insert fence instructions to prevent violating reorders. We automate fence insertion.
See the OOPSLA'15 paper and PODC'17 paper and DISC'19 paper.

Ongoing project: Certified Composable Concurrent Programming
We are building a certified concurrent collections library that supports atomic composition of method calls across objects.

Trust and Security

Ongoing project: Memory safety
Malicious attackers can use out-of-bound memory accesses to take over the whole system. We develop static and dynamic techniques to ensure that memory accesses are within bounds and within the access capabilities of the enclosing module.
See our NSF-supported project.

Static Analysis for Secure Cloud Computations
To protect user privacy, we encrypt data before processing it in the cloud. We apply type inference to find the most efficient encryption scheme.
See the OOPSLA'13 paper.

Trust Aggregation and Inference in Social Networks
Given local trust information between direct friends, we automatically infer a trust measure between any pair of users.
See the JCI'09 paper

Machine Learning

Learning Performance Models to Guide Synthesis of Efficient Concurrent Data Structures
Given a high-level relational specification of data, we want to automatically synthesize efficient concurrent data structures. Performance is an irregular phenomenon that can be only learned from experiments. We train neural networks as performance models. We use the performance model to choose the most efficient candidate from the space of possible candidate data structures.

Cooperation between Q-Learning Agents
We presented a technique for cooperation between heterogeneous Q-learning agents.
See the SMC'04 paper.

Programmable Biochemistry

Language and Type System for Programming Biochemistry
We introduce the BioScript domain-specific language for programmable biochemistry which executes on emerging microfluidic platforms and the ChemType type system that ensures that the chemical interactions are safe.
See the OOPSLA'18 paper.

Ongoing project: Drug Synthesis
Can we apply program synthesis techniques to automatically synthesize drugs with specified properties?


  Sponsors


NSF SHF CRII: Certified Byzantine Fault-tolerant Systems. M Lesani. 2017-2019
NSF SaTC: Practical Whole Kernel Memory Safety Enforcement. C. Song, M. Lesani. 2017-2020
NSF FET: Stochastic Synthesis of Peptides and Small Molecules. M. Lesani, P. Brisk, W. Grover. 2019-2022.
NSF CAREER: Distributed System Synthesis on Certified Middleware. M. Lesani. 2020-2025