close

Вход

Забыли?

вход по аккаунту

?

Untrustworthy Programming Languages

код для вставкиСкачать
Untrustworthy Programming
Languages
Andrew Kennedy, MSR Cambridge
Queen Mary, University of London, May 2005
1
Do you trust your
programming language?
пЃ¬
Modern programming platforms promise security:
пЃ¬
пЃ¬
The Java security model is based on a customizable "sandbox" in
which Java software programs can run safely, without potential
risk to systems or users (java.sun.com/security)
The .NET Common Language Runtime implements its own
secure execution model that is independent of the host platform
(Don Box, MSDN magazine)
пЃ¬
Most articles emphasise type-safety (=> memory safety)
of the JVM or CLR
пЃ¬
пЃ¬
And of course, special-purpose mechanisms such as Code Access
Security (stack-walking), permissions, crypto, etc
But that’s not the whole story…
Queen Mary, University of London, May 2005
2
The way it was
пЃ¬
In the past:
пЃ¬
пЃ¬
пЃ¬
пЃ¬
пЃ¬
programming language abstractions made languages “high-level”
i.e. far from the raw metal of the machine
good software engineering
protected programmers from themselves & others
If the language contained holes, it was “just” a
programming problem
In any case, nothing was enforced “underneath” except
at coarse boundaries (machine, system/user, process)
Queen Mary, University of London, May 2005
3
But now...
пЃ¬
The programming model is part of the security
model
пЃ¬
пЃ¬
in particular, its type system
but also, other aspects…
Programmers will assume that abstractions are
enforced underneath...
пЃ¬ ...and use them to write secure code.
пЃ¬
Queen Mary, University of London, May 2005
4
Eiffel, 1989
Cook, W.R. (1989) - A Proposal for Making Eiffel Type-Safe, in
Proceedings of ECOOP'89. S. Cook (ed.), pp. 57-70. Cambridge
University Press.
Betrand Meyer, on unsoundness of Eiffel:
“Eiffel users universally report that they almost
never run into such problems in real software
development.”
Queen Mary, University of London, May 2005
5
Ten years later: Java
Queen Mary, University of London, May 2005
6
Secure programming platforms
Java source
Java compiler
JVML (bytecodes)
Executed on
JVM
(Java Virtual
Machine)
Queen Mary, University of London, May 2005
C#
C# compiler
CIL
C++
C++
compiler
Visual Basic
VB
compiler
CIL
CIL
Executed on
.NET CLR
(Common Language Runtime)
7
Type safety
пЃ¬
Ensures
пЃ¬
пЃ¬
пЃ¬
Isolates software processes (“Application Domains” in
.NET)
пЃ¬
пЃ¬
data safety: can access memory only through typed objects
code safety: can access components only according to their
interface
used for downloadable plug-ins for UI in next version of
Windows
Importance of type safety is now widely appreciated
пЃ¬
Microsoft would issue an immediate “critical update” if a type
safety bug was discovered
[Insert war stories here]
Queen Mary, University of London, May 2005
8
Type loophole => anything goes
пЃ¬
Exploit a type loophole to execute arbitrary code. Here’s a recipe.
1.
Define a delegate type D, create a delegate object off an empty method
delegate void D();
public static void DoNothing() { }
D d = new D(DoNothing);
2.
Define a SpoofD class with int field spoofing the (internal) function pointer field
of the delegate type
class SpoofD { public int fptr; ... }
3.
Now pretend that the delegate object has type SpoofD (via type loophole)
SpoofD sd = ...loophole magic...(d);
4.
Set the spoof function pointer field to the address of your malicious code
sd.fptr = my_bad_code;
5.
Invoke the delegate
sd();
Queen Mary, University of London, May 2005
9
Beyond type safety
пЃ¬
How do programmers reason about security properties
of their code? Or about their code at all? We might
hope that:
пЃ¬
пЃ¬
A C# programmer can reason about code armed only with the
C# language spec and specs for libraries used by the code
Unfortunately, it seems that a C# programmer also
needs
1.
2.
3.
Some understanding of how C# is translated into IL
Some understanding of the behaviour of IL
Some understanding of parts of the standard library not
mentioned in the language spec or used by the program
Queen Mary, University of London, May 2005
10
Example 1: “Privacy through override”
пЃ¬
пЃ¬
In C# (and Java), overridden methods cannot be invoked directly
except by the overriding method
This property has been used by programmers for security purposes:
class InsecureWidget {
// No checking of argument
virtual void Put(string s);
…
}
class SecureWidget : InsecureWidget {
// Validate argument and pass on
override void Put(string s) {
Validate(s);
// Oh, yes we can! Direct call on superclass
base.Put(s);
ldloc sw
}
}
ldstr “Invalid string”
…
call void InsecureWidget::Put(string)
SecureWidget sw = new SecureWidget();
// We can’t avoid validation of arguments to Put, can we?
Queen Mary, University of London, May 2005
11
Analysis
пЃ¬
What went wrong?
пЃ¬
пЃ¬
пЃ¬
пЃ¬
What is a good way to characterize this?
пЃ¬
пЃ¬
пЃ¬
In C#, overridden methods can only be invoked through “base”
calls
In IL, they can be called directly
So there are programs in IL that can provoke behaviour not
possible from C#
Translation from C# to IL fails to be fully abstract
See “Protection in Programming Language Translation”, Abadi,
1998
How can we fix it?
пЃ¬
Not easily: IL was designed for multiple languages, with
conflicting goals
Queen Mary, University of London, May 2005
12
An ideal: full abstraction
пЃ¬
Ensure that all abstractions of the programming
language are enforced by the runtime
пЃ¬
пЃ¬
пЃ¬
programmers don’t have to know what’s underneath
if they understand the programming language, they understand
the platform programming model
Ensure that translation from C# to IL is fully abstract
Properties that hold
here...
...also hold here
Queen Mary, University of London, May 2005
C# program
IL program
13
Full abstraction
пЃ¬
Two programs are equivalent if they have the same
behaviour in all contexts of the language e.g.
class Secret {
private int f;
public Secret(int fv) { f = fv; }
public Set(int fv) { f = fv; }
}
пЃ¬
пЃ¬
≈
class Secret {
public Secret(int fv) { }
public Set(int fv) { }
}
A translation is “fully abstract” if it respects equivalence
For us:
пЃ¬
пЃ¬
the “translation” is from source language (C# etc) to MSIL
if there exist contexts (e.g. other code) in MSIL that can
distinguish equivalent source programs, then the translation fails
to be fully abstract
Queen Mary, University of London, May 2005
14
Full abstraction for Java
пЃ¬
пЃ¬
Translation from Java to JVML is not quite fully abstract
(Abadi, 1998)
At least one failure: access modifiers in inner classes
пЃ¬
пЃ¬
пЃ¬
a late addition to the language
not directly supported by the JVM
compiled by translation => impractical to make fully-abstract
without changing the JVM
Queen Mary, University of London, May 2005
15
Full abstraction for C#?
пЃ¬
A number of failures
Excuse: multiple languages target the CLR, with different goals
 The JVM was designed for a single language: Java. (Almost) Fullabstraction was probably an accident; though in retrospect it’s a good
thing.
пЃ¬
пЃ¬
For C#/CLR, we can catalogue failures of full abstraction and
propose fixes
пЃ¬
пЃ¬
пЃ¬
пЃ¬
either: change the translation from C# to IL
or: reduce expressivity of IL (fewer IL contexts)
or: increase the expressivity of C# (more C# contexts)
At least: document the failures, educate programmers, provide tools
to spot insecure programming patterns
Queen Mary, University of London, May 2005
16
Example 2
Encapsulation of object state
пЃ¬
Programmer expectation: instances of types whose API
ensures immutability are immutable.
пЃ¬
пЃ¬
Ex: String, DateTime, Int32
Boxing shouldn’t make any difference, should it?
// A dictionary keyed on strings
// Oh, yes we can! Just get pointer to interior
class StringDict {
ldloc salary
private Hashtable dict;
int32
public object Get(string s) { unbox
return
dict[s]; }
internal void Set(string s, object
{ … }
stind.i4 o)
1000000
…
}
static StringDict personalData;
// In a module far away…
// We cannot update from here
object salary = personalData.Get(“Salary”);
Queen Mary, University of London, May 2005
17
Example 2
Encapsulation of object state
пЃ¬
An equivalence that is not preserved:
public static int Foo(int x) {
object y = (object) x;
Bar(y);
return (int) y;
}
пЃ¬
≈
public static int Foo(int x) {
object y = (object) x;
Bar(y);
return x;
}
Fix?
пЃ¬
In CLR type system: disallow update after unboxing
Queen Mary, University of London, May 2005
18
Example 3
this is valid object instance?
пЃ¬
Instance methods are always invoked on a valid
instance, surely?
class Foo {
// Instance registered for privileged action
private static Foo registered = null;
// Only called from this module (internal access)
internal void Register() { registered = this };
public void Bar() {
if (this == registered) {
Oh, yes we can! Just call-direct-with-null
// Perform privileged //
action
ldnull
}
}
call void Foo::Bar()
}
// We can’t execute privileged action from another module
Queen Mary, University of London, May 2005
19
Example 3
this is valid object instance?
пЃ¬
An equivalence that is not preserved:
class C {
public bool Foo() {
return this != null;
}
…
}
пЃ¬
≈
class C {
public bool Foo() {
return true;
}
…
}
Fix?
пЃ¬
пЃ¬
In C# compiler: explicit check-for-null at start of method
In CLR: check-for-null at call-site (as with virtual call)
Queen Mary, University of London, May 2005
20
Example 4
Exceptions are instances of System.Exception?
try
{
// perform some action, to completion
} catch (Exception e)
{
// undo action whenever an exception was thrown in try-block
}
// Action either ran to completion, or was fully undone
// Not necessarily! From IL, can throw any object
newobj instance void System.Object::.ctor()
throw
Queen Mary, University of London, May 2005
21
Example 5
Booleans are two-valued?
void Foo(bool b)
{
bool c = !b;
if (!c != b)
{
Console.WriteLine(“This cannot happen”);
}
}
// Oh yes it can!
ldc.i4 2
call void Foo(bool)
Queen Mary, University of London, May 2005
22
Example 5
Booleans are two-valued?
пЃ¬
An equivalence that is not preserved:
static bool Foo(bool x, bool y)
{
return x==y;
}
пЃ¬
≈
static bool Foo(bool x, bool y)
{
return (x == false) == (y == false);
}
Fix?
пЃ¬
Change C# compilation of == and != for bool so that it cares
only about zero/non-zero-ness
Queen Mary, University of London, May 2005
23
Weak abstractions
пЃ¬
Some abstractions aren’t broken; they’re just a bit weak
пЃ¬
arrays are always mutable
пЃ¬
пЃ¬
developers forget this and define “readonly” properties with array
types
run-time types break “privacy by subsumption”
solution to array problem would be to return array as an
IEnumerable (a read-only enumerator)
 but run-time types let programmer “cast” back to the array
пЃ¬
пЃ¬
Other abstractions are broken not by IL but by library
classes
пЃ¬
e.g. delegates (closures) would “encapsulate” code & object
state if it weren’t for System.Delegate.Target and
System.Delegate.Method methods.
Queen Mary, University of London, May 2005
24
Why bother?
пЃ¬
Even if the translation from C# to IL were fully abstract,
reasoning about C# programs would still be hard.
пЃ¬
пЃ¬
пЃ¬
пЃ¬
пЃ¬
Programmers make mistakes in writing secure code
Tools for automating reasoning about programs are still in their
infancy
There are many other pitfalls in the language
So why bother about full abstraction?
Because it’s a great starting point:
пЃ¬
пЃ¬
The ability to reason about C# programs “in C#” is hugely
simplifying
Even better: if we could cut down to a subset of C# that suffices
Queen Mary, University of London, May 2005
25
Formalize?
пЃ¬
пЃ¬
пЃ¬
пЃ¬
Proofs of full abstraction are hard
We don’t have a complete formal model of C#
We don’t have a complete formal model of IL
So what to do?
пЃ¬
пЃ¬
Optimist: even if we can’t formalize, we can identify failures, and
fix them all
Pessimist: we can never be sure that we have full abstraction.
Instead, focus on certain patterns, prove that these are
watertight. Example:
prove that integers are safe!
 prove that private fields don’t leak
пЃ¬
Queen Mary, University of London, May 2005
26
Conclusions
The programming model is a vital part of the security
story for .NET and Java
пЃ¬ Programmers need to know what they can trust
 “Full abstraction” is the ideal
пЃ¬
пЃ¬
пЃ¬
пЃ¬
пЃ¬
пЃ¬
My choice would be to fix the holes we know about
Might be hard to do
If we can’t or won’t, we should educate developers
Type safety is now taken for granted as a necessity
In the future, full abstraction also?
Queen Mary, University of London, May 2005
27
Документ
Категория
Презентации
Просмотров
3
Размер файла
926 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа