MCP servers that leak by accident

The problem

What we built

• Three MCP servers with the same four tools over the same product catalog: the official Python SDK written the usual way, a hardened Python version with a public view and server-side quoting, and Synsema with information-flow labels.
• In all three, a fourth tool, "added later for the purchasing team", returns the whole record.
• A side-by-side test bench calls every tool on the three servers, and any MCP client (Claude Code, Cursor) can connect to them.

Results

The code, side by side

def product_detail(id: int) -> dict:
    """(Added later, for the purchasing team.) Full product detail."""
    return c.find(id)   # the slip: returns the whole record, and nothing prevents it

task load_confidential()
    let raw be json_decode(read_file("./cases/01-mcp-servers/data/catalog.json"))
    let conf be {}
    each p in raw
        set conf[text(p.id)] to {"cost_usd": private(p.cost_usd, "company"), "supplier": private(p.supplier, "company"),
            "min_margin_pct": private(p.min_margin_pct, "company"), "max_discount_pct": private(p.max_discount_pct, "company"),
            "internal_note": private(p.internal_note, "company")}
    give conf

-- (Added later, for the purchasing team.) The same slip as in Python: returns the whole record.
-- In Synsema it never reaches the model: the HTTP response is a public output and refuses labeled fields.
task t_product_detail(args)
    give merge(find(args.id), CONFIDENTIAL[text(args.id)])

Why Synsema

• Confidential values are labeled once, when loaded. Every value computed from them carries the label.
• Any public exit (the HTTP response, a log, a file) refuses a labeled value unless the code calls declassify with a reason, and that reason is logged.
• synsema code check lists every declassify with its line before anything runs. That list is the security review.

What it does not solve

• Labels are opt-in: the server must run with serve --labels. Without the flag, private() fails on purpose instead of running unprotected.
• Propagation is conservative. Reading public fields from a list that also holds private values gives a private result, so public and confidential data must live in separate structures.
• A violation returns HTTP 500, not a tidy JSON-RPC error. It cannot be caught, because catching it would leak one bit per try.
• Labels protect confidentiality, not authorization. If quoting is allowed, the model can still ask for the maximum discount.

Share