Language-based-Security
< استفاده از مطالب سایت فراکنش با ذکر منبع مجاز است.>
END-TO-END 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

THE MODEL
FM = < N, P, SC, Å, ® >
N = { a, b, … }: a set of logical storage objects or information containers: files, segments, program variables, and also users.
P = processes. “Processes are the active agents responsible for all information flow.”
ادامه مطلب و دانلود فایل مقاله
References
David Aspinall, Secure Programming Lecture 15: Information Leakage, Edinburgh University, March 2016.
Sabelfeld and Myers, Language-Based Information-Flow Security, Cornell University, 2003.
Drayton Benner, A Lattice Model of Secure Information Flow by Dorothy Denning, 2000.
Dorothy Denning & Peter Denning, Certification of Programs for Secure Information Flow, Communications of the ACM (CACM) 1977
Anupam Datta, Language-based Security: Information Flow Control, Carnegie Mellon University, 2009.