Shifa — Online Security Analyzer

Getting Started with Shifa

What is Shifa?

Shifa is a static analysis tool for C programs that combines Separation Logic (for memory safety) with Information Flow Analysis (for security properties). It uses Z3 as its SMT solver backend.

Unlike dynamic tools (sanitizers, fuzzing), Shifa reasons about all execution paths statically, providing formal guarantees about information flow.

Security Levels

Shifa uses a two-level security lattice:

Hi (High / Secret) — confidential data that must not leak
Lo (Low / Public) — data that may be publicly observable

The core property: information must never flow from Hi to Lo. Shifa detects both explicit flows (direct assignment) and implicit flows (information leaked through branch conditions).

How to Use the Playground

Pick a demo from the dropdown, or write your own C code in the editor.
Write stubs in the right editor to declare security levels for function parameters and global variables.
Set the entry function — Shifa analyzes starting from this function.
Choose a mode:
- IFA — Information Flow Analysis (detects Hi→Lo leaks)
- CT — Constant-Time analysis (detects secret-dependent branches and array indices)
- MS — Memory Safety only (separation logic, no security)
Click Run Analysis and inspect the output.

Understanding the Output

In IFA mode, look for:

LEAK — a Hi value flows to a Lo sink (violation!)
ReturnHi — function returns Hi when spec says Lo
OK — no security violation found

In CT mode, additionally:

[VIOLATION] BranchCond — secret-dependent branch (timing leak)
[PROTECTED] ArrayIndex — secret array index (cache side channel)
[REPAIRED] — violation mechanically repaired by CT transformer

Example: Detecting a Secret Leak

Consider a password checker:

int check(int secret, int guess) {
    if (secret == guess)
        return 1;
    else
        return 0;
}

With the stub spec check(Hi, Lo) -> Lo;, Shifa detects that the return value depends on the Hi branch condition — an implicit flow violation.

Try the Demos

Start with the curated demos in the dropdown. Each one demonstrates a different analysis capability:

Basic Information Flow — simple function call chains
PQC Key Handling — mixed-security array regions (safe vs. leak)
Implicit Flow — information leaked through branches
Parallel Tenants — pthread-based multi-tenant isolation
Constant-Time — detecting timing side channels

Stub Language Reference

Shifa uses .slstub files to declare security policies and memory contracts for functions and global variables. This is how you tell Shifa what is secret and what is public.

Security Specifications (`spec`)

Declare parameter and return security levels for functions:

// Parameters: (Hi, Lo) means first arg is secret, second is public
// Return: Lo means the return value must be public
spec my_function(Hi, Lo) -> Lo;

If a Hi value flows to a Lo return, Shifa reports a LEAK.

Global Variable Classification (`classify`)

// Entire variable is secret
classify global secret_key : Hi;

// Entire variable is public
classify global output_buf : Lo;

// Array with mixed regions: indices 0-31 are Hi, 32-127 are Lo
classify global pk : *[0:31]Hi [32:127]Lo;

Memory Stubs (`stub`)

Separation Logic pre/post conditions for library functions:

// malloc: no precondition, postcondition gives a fresh pointer
stub malloc(n: int) {
  requires emp;
  ensures $ret -> _;
}

// free: requires a valid pointer, deallocates it
stub free(x: ptr) {
  requires x -> _;
  ensures emp;
}

// memcpy: source must be allocated, stays allocated after
stub memcpy(dst: ptr, src: ptr, n: int) {
  requires src -> _;
  ensures src -> _;
}

Parallel Dispatch (`parallel`)

// Mark a function as launching parallel tasks
parallel dispatch;

Linked List Shapes (`list_struct`)

// Tell the loop invariant engine about linked-list structures
list_struct Node next;

Formula Syntax

`emp`	Empty heap
`x -> _`	x points to some value
`x -> {f:v}`	x points to struct with field f = v
`f1 * f2`	Separating conjunction (disjoint heaps)
`ls(x,y)`	Linked list segment from x to y
`arr(x,lo,hi)`	Array from index lo to hi
`$ret`	Return value

Complete Example

// Security policy for a crypto library
classify global master_key : Hi;
classify global public_buf : Lo;

spec encrypt(Hi, Lo) -> Lo;
spec decrypt(Hi, Lo) -> Hi;

stub malloc(n: int) {
  requires emp;
  ensures $ret -> _;
}

stub free(x: ptr) {
  requires x -> _;
  ensures emp;
}

About Shifa

Overview

Shifa (Symbolic Heap-based Information Flow Analyzer) is a static analysis tool for C programs that formally verifies security properties. It combines two complementary techniques:

Separation Logic — reasons about memory safety (use-after-free, null dereference, buffer overflow) using bi-abductive inference
Information Flow Analysis — tracks how data classified as secret (Hi) propagates through the program and detects unauthorized flows to public (Lo) sinks

Unlike dynamic tools (sanitizers, fuzzing), Shifa reasons about all execution paths statically, providing sound guarantees. It uses Z3 as its SMT solver backend for constraint solving.

Analysis Modes

IFA	Information Flow Analysis — detects explicit flows (direct assignment of secret to public) and implicit flows (secret leaked through branch conditions). Supports `declassify` for modeling one-way functions like hashing.
CT	Constant-Time Analysis — detects secret-dependent branches (timing side channels) and secret-dependent array indices (cache side channels). Can mechanically repair violations using `__builtin_ct_select`.
MS	Memory Safety — pure separation logic analysis without security annotations. Verifies pointer safety, memory allocation/deallocation, and absence of dangling pointers.

Key Features

Bi-abductive inference — automatically infers frame conditions and missing preconditions, enabling compositional analysis of large programs
Inter-procedural analysis — tracks information flow across function calls, including through global variables and output parameters
Mixed-security regions — supports arrays with different security levels at different index ranges (e.g., a key pair with public and secret components)
Parallel analysis — detects data races and information leaks in concurrent code with parallel dispatch
Stub specifications — declarative .slstub language for specifying security policies and memory contracts for library functions

Technical Foundation

Shifa is built on established formal methods research:

Separation Logic (Reynolds, O'Hearn) — compositional heap reasoning with the frame rule
Bi-abduction (Calcagno et al., POPL 2009) — simultaneous inference of preconditions and frame, as used in Facebook Infer
Non-interference (Goguen & Meseguer, 1982) — the security property that high-security inputs cannot influence low-security outputs

The analyzer is implemented in OCaml (~30,000 lines) and uses Z3 for satisfiability checking of separation logic entailments and arithmetic constraints.

Author

Shifa is developed by Mahmudul Faisal Al Ameen.

Version

Shifa v0.3.0 — This playground runs the full analyzer in the cloud. Source code is not yet publicly available.