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).
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.
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
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.
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.
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.
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.
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
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.
see for Brian K
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.
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.
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