Language-based-Security

End-to-end security (confidentiality, integrity) is a general need

End-to-end security requirement: protection at all levels

So we need application level protection

TRADITIONAL APPROACH TO SECURITY

Typical security solutions are not enough.

• Encryption

—Pro: secures a communication channel

—Con: but not the endpoints, where data enters or leaves

• (Application) Firewalls

—Pro: stop some bad things entering programs

—Con: massive leakage via application ports 21, 23, 80

• Access control (ACLs) in the OS

—Pro: isolates users, files, processes

—Con: what if one part of a process should be protected from parts of the same process?

• Anti-virus

—Pro: Good with known malware, recognize by signature

—Con: Little use on zero-day exploits

• Code signing

—Pro: Digital signatures identify code producer/packager

—Con: Don’t actually guarantee code is secure

• Sandboxing and OS-based monitoring

—Pro: Can block low-level accesses

—Cons:
– Can not block information transfer within applications
– Pure sandboxes too strict (may prevent information sharing)

•The above mechanisms check release of data but not data propagation

LANGUAGE-BASED SECURITY (LBS)

• Idea: prevent application-level attacks inside the application.

• Advantages:

—Semantics-based security specification:

     – exact and precise definition of what is required, based on definitions and data used inside program.

• Static enforcement sometimes possible if we can

 – examine the code (white box technique),

– And use programmer annotations and/or special type systems,

– Or force run-time monitoring if needed.

INFORMATION FLOW ANALYSIS

• Information Flow (IF) analysis:

—How the information flow inside programs: is there a secret “going out” of the system?

• Information Flow policies

—The focus can be on confidentiality or integrity

• Information Flow controls

—Mechanisms that implement the above policies

• Active research field (studied for ~ 40 years)

• IF-based Compilers

—JIF (Java) 2001-2009 (Cornell University)

—FlowCaml (ML) 2002 (INRIA)

• Limited impact on practice!

LANGUAGE-BASED SECURITY (LBS)

• Language-based security (LBS) approaches:

—Taint tracking (dynamic)

—Type checking (static)

DYNAMIC TAINT TRACKING

• Idea: add security labels to data inputs (sources) and data outputs (sinks). Propagate labels during computation (cf dynamic typing).

Labels are:

• Tainted

—Data from taint sources (e.g., user input)

—Data arising from or influenced by tainted data

• Untainted

—Data that is safe to output or use in sensitive ways

• Disadvantages:

• “Preventing code injection exploits using dynamic taint tracking is like letting a thief in your house and checking his bag for stolen goods at the very moment he tries to leave. It might work, but only if you never lose track of the gangster and if you really know your house. However, I would prefer a solution that does not let thieves in my house in the first place.”

—Martin Johnsused, dynamic taint tracking, 2007

• implicit flows

LANGUAGE-BASED SECURITY (LBS)

• Many security models are based on abstract formalisms

—Typically, state machines [Bell-LaPadula73, Goguen-Meseguer82,84,Rushby81]

—Challenge: accurately relating formal security specification to concrete implementations

• Denning & Denning proceed from a new (at the time 1977) starting point: language-based security

—Define security certification of programs at the language level

—Compile-time, completely automated process

—Goal: If program p is certified by the compiler, then it is secure

TERMINOLOGY: COVERT CHANNELS

• Channel: a mechanism for signaling information through a computing system

• Covert channel: a channel whose primary purpose is not information transfer

TYPES OF COVERT CHANNELS

• Implicit flows: signal information through the control structure of a program

• Termination channel: signal information through the termination or nontermination of computation

• Timing channel: signal information through the time at which an action occurs rather than through the data associated with the action

• Probabilistic channel: signal information by changing the probability distribution of observable data

• Resource exhaustion channel: signal information by the possible exhaustion of a finite, shared resource

• Power channel: embed information in the power consumed by the computer

SECURITY PROPERTIES

• What kinds of properties do we want to ensure programs or computing systems satisfy?

• “Nothing bad ever happens” or
“Something bad must not happen”

—E.g.: system should not crash

• A property that can be enforced using only history of program

• Amenable to purely run-time enforcement

• Examples:

—access control (e.g. checking file permissions on file open)

—memory safety (process does not read/write outside its own memory space)

—type safety (data accessed in accordance with type)

LIVENESS PROPERTIES

• “Something good eventually happens” or
“Something good must happen”

• Example: availability

—“The email server will always respond to mail requests in less than one second”

—“Every packet sent must be received at its destination”

•Violated by denial of service attacks

• Can’t enforce purely at run time

• Tactic: restrict to a safety property

—“web server will respond to page requests in less than 10 sec or report that it is overloaded.”

“INFORMATION FLOWS” ATTRIBUTE

• “xÞy” means that information flows from x to y

—this is the attribute calculated during certification

• Explicit flow: e.g., “y := x” implies “xÞy”

• Implicit flow: “y := 1; if x=0 then y:=0”

—Assuming x is 0 or 1, then x=y after completion

—\ xÞy

—Generally, control structures in language cause such indirect/implicit flows

• Transitive: xÞy and yÞz implies xÞz

• Defn. Program statement specifies a flow if its execution could result in flow

• N.b., this is weaker than “does result in flow”

SECURITY REQUIREMENTS

• Program p is secure iff flow xÞy results from executing p only when x®y

—Security Definition (1st shot): flow xÞy results from executing p only when x®y

• Undecidable: is there a flow from x to y in “if f(x) halts then y:=0”?

• Security Definition: flow xÞy is specified by p only when x®y

—note that “is specified by” is weaker than “results from executing”

• Living with imprecision:

—“if x=0 then if x¹0 then y:=z” is disallowed if z®y

INFORMATION FLOW POLICY AS LATTICE