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).

You can define custom labels that map to this lattice using lattice Lo_name <= Hi_name;. For example, lattice Trusted <= Untrusted; for privilege isolation, or lattice Public <= Secret; for data classification.

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!)
LEAK [Integrity] — untrusted (Hi) data written to protected (Lo) resource
LEAK [SecretRemnant] — secret data not erased before free()
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
Memory Safety — separation logic verification (swap, use-after-free)
Secret Remnant — secret data not erased before free
Privilege / Integrity — Biba dual with custom lattice labels
Custom Lattice — domain-specific security labels
Syscall APIs — 7-function kernel-user isolation system (insecure vs. secure vs. user-space)

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;

Custom Security Labels (`lattice`)

Define domain-specific names for security levels instead of raw Hi/Lo:

// Privilege isolation
lattice Trusted <= Untrusted;
classify global kernel_buf : Trusted;
spec handle_syscall(Untrusted) -> Trusted;

// Data classification
lattice Public <= Secret;
spec encrypt(Secret) -> Public;

The left label maps to Lo (low/protected), the right to Hi (high/untrusted). You can use declassify with custom labels to model sanitization.

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. It is based on theories with soundness guarantees — Separation Logic for memory safety and information flow analysis for security. 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). Also supports integrity/privilege checking via the Biba dual (untrusted → protected = violation). Supports `declassify` for modeling sanitization and one-way functions.
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
Secret remnant detection — detects when secret data is not erased before memory deallocation (free), preventing heap inspection vulnerabilities (CWE-244). This check is derived from the IFA lattice: deallocation transitions memory from any security level to Lo, so Hi data at a free site triggers a confidentiality violation
Declassify — models one-way functions (hashing, HMAC) that intentionally downgrade secret data to public, preventing false positives on legitimate cryptographic transformations
Constant-time mechanical repair — automatically rewrites secret-dependent branches using __builtin_ct_select and secret-dependent array indices using value barriers, producing timing-safe shadow functions
Custom security lattice — define domain-specific security labels with lattice Lo_label <= Hi_label; instead of raw Hi/Lo. Examples: Trusted <= Untrusted for privilege isolation, Public <= Secret for data classification. Labels map to the built-in two-point lattice internally
Integrity / privilege checking — via the Biba dual interpretation: label untrusted data as Hi and protected resources as Lo. Any flow from untrusted (Hi) to protected (Lo) is caught as an integrity violation. Combined with declassify, this models input sanitization/validation
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.

Acknowledgements

The foundation of Shifa was built on research and tools developed in collaboration with:

Prof. Makoto Tatsuta — National Institute of Informatics, Tokyo
Prof. Chin Wei Ngan — National University of Singapore
Prof. Koji Nakazawa — Nagoya University
Prof. Daisuke Kimura — Toho University
Dr. Adi Prabawa — National University of Singapore
Benedict Lee

Their work on separation logic, bi-abductive inference, and entailment checking forms the core analytical engine upon which Shifa’s security analysis is built.

Version

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