# CMSC 838Y Paper Reviews

Skip down to paper 0: Michael Hicks, Stephanie Weirich, and Karl Crary. Safe and flexible dynamic linking of native code. In Robert Harper, editor, Proceedings of the ACM SIGPLAN Workshop on Types in Compilation, volume 2071 of Lecture Notes in Computer Science. Springer-Verlag, September 2000. [ .pdf ]

### Reviews for paper 0

#### Review from Nikhil Swamy <nswamy@cs> at Mon Feb 10 17:56:54 EST 2003:

This paper describes the design and implementation of a type-safe dynamic
linker/loader. The paper presents the notion of a Trusted Computing Base (TCB)
for a programming environment and in particular the existence of small and
provably safe TCB for the typed assembly language (TAL). In the design of their
dynamic loader the authors chose to design their loader as a type-checking and
linking module external to this TCB. This choice allows the demonstration of a
provably  safe method of dynamic loading since an unsafe module that is
attempted to be linked and loaded will be rejected by a verifier within the TCB
that is known to be sound.

In presenting some of the theoretical underpinnings of their design decisions,
the authors refer to some formal constructs for the representation of types
(Crary's \lambda_R) amd some of the specific type semantics of TAL
(type-erasure). Unfamiliarity with these constructs makes it difficult to
appreciate significance of the specific nature of this approach in contrast to
the basic intuitive approach suggested by the load_0. The analysis of the DLPop
library, however, provides allays some of the confusion by grounding the
discussion in concrete terms. In particular, the contrast of the DLPop
implementation against the somewhat familiar DLOpen libraries is instructive.

The paper concludes by establishing the case that DLPop meets the additional
design objectives of flexibility (TAL/Load is claimed to be able to work on
variants ranging from Java to OCaml) and efficiency (measurements suggested
performance comparable to existing methods).

#### Review from Yuan Yuan at Mon Feb 10 20:58:33 EST 2003:

Paper review: Safe and Flexible Dynamic Linking of Native code

This paper builds a complete framework for programming type-safe dynamic
linking of verifiable native code in context of TAL. Comparing with the flawed
performs two procedures: Disassembly and verification without addition to the
TCB of TAL. In this framework, authors demonstrate interface and usage of
DLpop, a type-safe version DLopen. To implement Dlpop in TAL/load, the object
file need to main a GOT for all dynamically loadable file in verifiable
language, TAL. And since the compiler adds a special dyninit function
consisting only of TAL code, all linking operations are type-safe. Security and
flexibility can be achieved by add dyninit function.

Authors also point out the new design have benefits of safety and applicability
with competitive overhead. In the end, many clues about how to use this
framework in different language to support dynamic linking are given out.

It is a long paper.) The main contribution is constructing the framework
supporting type-safe dynamic linking. A concrete demonstration using DLpop
makes the framework easier to understand. The key ideas of this framework are
using TAL to provide explicit type information for safety, placing small
procedure out of TCB to achieve flexibility. But in the related work section,
the talking about how to implement the framework in other languages is relative
brief; seems to abstract for me to understand.


#### Review from plamba@wam.umd.edu at Tue Feb 11 00:02:24 EST 2003:

This paper presents the design and implementation of flexible and safe dynamic
linking of native code. The approach explained in this paper is based on
verifiable native code. This system is developed on TAL. In the early section
of the paper author describes his approach towards the implementation and
design methodology. In this section author gives convincible arguments on the
problems of primitive load. According to the new approach described in the
paper loaded modules are to be closed. Smaller components are placed in TCB.
Authors points out the difficulty in closing the modules with respect to typed
names and presents the solution for this .The TAL/Load consists of two major
functions Disassembly and Verification.

following the verification. This paper presents the practical implementation of
the theory explained in the paper. It shows the implementation of DL pop that
is type safe version of the DLopen. In the later part of the paper it gives the
comparison between the Overheads of DL open with that of DLpop. These overheads
of the paper there is a brief description of  the other linking strategies like
DLL,COM etc


#### Review from Piyush Bhagat <piyushb@glue.umd.edu> at Tue Feb 11 11:52:32 EST 2003:

The paper presents a case of safe dynamic linking of the native code.The
approach of the paper is based on Typed assembly language(TAL) and the authors
implement dynamic linking without expanding the trusted computing base,on TAL
which was not done before.Inspite of the bytecode as is done in java by the JVM
and the JIT compilers the authors have taken a different approach ie of
verifiable native code in the paper.The paper underlines three basic
functionalities expected of a dynamic linking system. They are security,

For dynamic linking the authors have used DLpop which is nothing but a typesafe
version of DLopen.The paper describes the DLpop implemention in detail and its
differences with the ELF approach.The paper finally talks about the time and
space overheads imposed by the DLpop and load.The paper goes into great detail
describing each and every time overhead.This is think is particularly important
as these overheads reduce efficieny which I think is one of the most important
if not the most important quality expected of a dynamic linker.    

#### Review from Bryan Payne <bdpayne@cs> at Wed Feb 12 20:58:49 EST 2003:

This paper described a methodology and an implementation for type safe dynamic
linking of native code.  Overall, the paper was presented at a nice level,
taking the reading through the design, implementation and testing of the idea.
It was particularly nice to see the implementation and testing phase as I feel
that this helps to solidify the work.

In general, I liked the ideas presented in the paper and feel that it's a step
in the right direction.  However, as is often the case with work like this, it
also left open many additional areas of research.  These areas are mainly where
the authors needed to simplify the problem in order to come up with a solution
that allowed for a small TCB.  And, while this was necessary for this stage of
the work, it would be nice to see work like this continued in order to come up
with techniques that might all for less simplifications while still maintaining
a small TCB.

The performance testing portion of this paper looked at how the code performed
against the standard ELF libraries.  This was done by looking at different
overhead, etc).  While the numbers in these sections were interesting, and made
a good case for the performance on the DLpop technique, I felt that a little
more detail would have been useful.  Specifically, under the load-time
time could involve loading the library from disk (although it could be cached
in a variety of places as well...thus making the load time faster).  It would
be interesting to see a breakdown of the results in terms of what each portion
of the load-time is actuallying doing (e.g., 10ms for action A, another 25ms
for action B, etc).  In a similar fashion, it would have been nice to see
additional detail for the other performance testing as well (although, it is
admitidly hard to get accurate & useful performance testing numbers).

Overall, the paper presented a nice technique that I feel is worthy of
continued research in order to broaden its application and perhaps take a more
detailed look at it's performance attributes.

#### Review from Polyvios Pratikakis <polyvios@cs> at Thu Feb 13 10:54:08 EST 2003:

In this paper the authors present an extension to TAL that adds dynamic loading
capabilities, without losing safety. First, the current way for typechecking
dynamic code is presented, and it's flaws are underlined. The paper proposes a
different way to check dynamic code for safety, based on 3 restrictions, in
addition to avoiding using only name-comparison for types.
Next, a way to implement the system is presented briefly, along with it's API,
followed by the details of (one of the two) specific implementation of the
authors. Finally, measurements on both time and space overhead are used to
support that the safety gained is worth the (small) efficiency lost.
Concluding, there is a section on related work, and further references on

Overall, the paper looked a lot like a technical report, as it focuses more on
implementation issues than the corresponding theory. Also, it presupposes
report for the theoretical part. In general, What this paper offers is not an
extension of type-systems, but rather it's application in that specific way.
That is why the authors do not devote a large part of it in describing the
type-system of TAL or DLpop.

#### Review from Nathaniel Waisbrot <waisbrot@cs> at Thu Feb 13 11:27:22 EST 2003:

	This paper ties together our previous readings, adding dynamic linking to the
Typed Assembly Language.  As both Wadler's paper and Hicks, Weirich, and Cary
point out, reducing the amount of trusted code improves the safety of the
environment.  Therefore, their TAL extensions attempt to be as small as
possible, and dynamic linking is then built from the small trusted base in a
safe manner.
modules can't be statically type-checked.  Therefore, it is highly desirable to
find ways of making dynamic linking safe.

#### Review from Mr.Prashant Lamba<plamba@wam.umd.edu> at Thu Feb 13 11:55:21 EST 2003:

This paper presents the design and implementation of flexible and safe dynamic
linking of native code. The approach explained in this paper is based on
verifiable native code. This system is developed on TAL. In the early section
of the paper author describes his approach towards the implementation and
design methodology. In this section author gives convincible arguments on the
problems of primitive load. According to the new approach described in the
paper loaded modules are to be closed. Smaller components are placed in TCB.
Authors points out the difficulty in closing the modules with respect to typed
names and presents the solution for this .The TAL/Load consists of two major
functions Disassembly and Verification.

following the verification. This paper presents the practical implementation of
the theory explained in the paper. It shows the implementation of DL pop that
is type safe version of the DLopen. In the later part of the paper it gives the
comparison between the Overheads of DL open with that of DLpop. These overheads
of the paper there is a brief description of  the other linking strategies like
DLL,COM etc



#### Review from Brian K at Thu Feb 13 12:11:12 EST 2003:

The goal of the paper is to build a system for provably correct type
checked dynamic linking on top of Typed Assembly Language (TAL) while
minimizing changes to the 'Trusted Computing Base'. The majority of
linking is moved entirely outside of the TCB.  A load function is
implemented in TAL which manages type checking and verification, which is
in turn used to implement an anologue to the C dynamic linking api.

The key is the dyninit function which is exported by every module and
calle don loading .  The function fills in the current GOT with standard
exports of the module.  Export information and the GOT are all updated
inside of the running code.  To the linker, the only function which any
module actually exports is the dyninit function.  Because this function
will always be present with a constant signature it can be linked
statically to avoid dynamic avoid type checking issues.  This method
allows flexibilty as the data structure for the GOT is not hard coded in
the TCB and benefits from TAL typechecking since dyninit runs as user
code.

symbol exports this method produces smaller modules compared to ELF since
the symbol table is not included in the file but rather built dynamically
at link time.  Runtime is slightly slower than ELF as the table needs to
be built, but in general any slowdowns are overshadowed by the validation
system.



#### Review from Brian K is Brian Krznarich <bjkrz@cs.umd.edu> at Thu Feb 13 12:12:08 EST 2003:

see for Brian K

#### Review from Jeff Odom <jodom@cs.umd.edu> at Thu Feb 13 12:16:51 EST 2003:

The authors in this paper describe a framework for providing type-safe dynamic
linking of Typed Assembly Language (TAL).  The claim they make is, essentially,
that if type safety is desirable, and dynamic linking is also desirable, then a
combination of the two is also desirable.  One of the key sticking points in
the paper it seemed was a consideration of security; namely, that adding
dynamic linking to a type-safe framework should only minimally add to the
trusted code base (TCB), thereby reducing the likelyhood of security violations
of the framework.  This seemed to make a case for "real-world" applicability in
much the same way as Java's "sandboxing" does.  Lastly, the cases made for
(Java, DLLs, COM, etc.) was something not often found in papers of this type
but shows well the applicability of this technique and provides interesting
insights into lines of future work.

#### Review from James Rose <rosejr@cs> at Thu Feb 13 12:22:45 EST 2003:


This paper presents an extension of Typed Assembly Language
statically named imports to their locations in shared libraries.  The
term "dynamic linking" can refer to both, though the two differ
substantially in generality.  Anyway, what this paper offers is a way
to load modules at run-time while preserving the type safety offered
by TAL.  In this case, run-time linking requires that the type of
imports be known statically, but the symbol name and the location of
the object code are decided dynamically.  This is one design decision that
keeps the implementation simple.  The essential contribution
of this paper is a series of design decisions which extend the
flexibility of TAL while preserving its benefits: type safety, native
code, and a small trusted computing base.


#### Review from Mujtaba Ali <mujtaba@bitsmart.com> at Thu Feb 13 12:27:39 EST 2003:

Being an extremely long article, it?s difficult to sum up my thoughts
concisely.  I enjoyed how the article provided concrete examples to back up the
?theory?.  I also enjoyed how the article presented alternate approaches and
explained why these approaches were not optimal.  The explanation of the
acronym TCB, and the importance of having a small TCB, was handled well and I
feel this is a concept that will come up again and again.

The article was successful in hammering home the point that TAL was not
significantly modified to support source-level dynamic linking - rather a few
enhancements were introduced and used to _program_ dynamic linking. What
particularly struck me as amazing, and what I still don?t fully understand, is
how one implementation of dynamic linking can be used for different source
languages, each with their own linking peculiarities.



Generated: Thu Mar 6 15:39:24 EST 2003 by mwh

mwh@cs.umd.edu

Web Accessibility