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 
means of adding dynamic linking in TAL, the key process, load, in TAL/Load 
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 
components outside of TCB to support dynamic linking, extracting linking 
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.

The concept of load is well defined in the paper loading which is the process 
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 
are Time Overhead (Run-Time Overhead, Load Time Overhead) and Space. In the end 
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, 
flexibility and efficiency.The authors have made several small additions to TAl 
to enable dynamic linking rather than adding them to the TCB.

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 
aspects of the performance (run-time overhead, load-time overhead, space 
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 
overhead...it wasn't clear exactly what was being measured.  Typically, load 
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 
dynamic linking.

Overall, the paper looked a lot like a technical report, as it focuses more on 
implementation issues than the corresponding theory. Also, it presupposes 
detailed knowledge of the reader about the TAL system, and links to a technical 
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.
	Dynamic linking has many advantages over static linking (smaller footprint, 
potential for faster loading, etc.), but it's also dangerous because the 
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. 

The concept of load is well defined in the paper loading which is the process 
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 
are Time Overhead (Run-Time Overhead, Load Time Overhead) and Space. In the end 
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.

Coments are made about speed and space overhead.  For moderately sized      
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 
adding or improving the dynamic-linking type-safety of other technologies 
(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
which allows run-time linking.  I use the term "run-time linking" to
distinguish it from "load-time linking"; that is, the binding of
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