Going Deep

Chris Hawblitzel and Juan Chen: Introduction to Typed Assembly Language (TAL)

Download this episode

Download Video

Description

Typed Assembly Language (TAL) extends traditional untyped assembly languages with typing annotations, memory management primitives, and a sound set of typing rules. These typing rules guarantee the memory safety, control flow safety, and type safety of TAL programs. Moreover, the typing constructs are expressive enough to encode most source language programming features including records and structures, arrays, higher-order and polymorphic functions, exceptions, abstract data types, subtyping, and modules. Just as importantly, TAL is flexible enough to admit many low-level compiler optimizations. Consequently, TAL is an ideal target platform for type-directed compilers that want to produce verifiably safe code for use in secure mobile code applications or extensible operating system kernels. [Source]

You've met Microsoft research scientist and operating system expert Chris Hawblitzel before. He's the architect and lead researcher of the Verve operating system research project from MSR. As you learned in that interview, typed assembly language and Hoare logic were employed to verify the absence of many kinds of errors in low-level code. Chris et al. use TAL and Hoare logic to achieve highly automated, static verification of the safety of Verve. We didn't spend much time on TAL during the Verve interview, so we decided to remedy that. Enter computer scientist and RiSE team member Juan Chen who did much of the TAL work for Verve. After you watch this video, you should read this paper to go much deeper.

Tune in and get a sense of what TAL is, how type verification works for assembly code, benefits, trade-offs, and much more. Enjoy.

Embed

Format

Available formats for this video:

Actual format may change based on video formats available and browser capability.

    The Discussion

    • Justin Bailey

      Great video! Juan Chen has done some really impressive work. In particular, she formalized a big chunk of the Sparc instruction set. Yes, typed machine language Smiley

      Greg Morrisett's papers are worth reading. I found "TALx86: A Realistic Typed Assembly Language" to be the most accessible (http://www.cs.cornell.edu/talc/papers.html).

      Atsushi Ohori wrote a paper that treats typed machine languages as proof systems. Very abstract but impressive too: "A Proof Theory for Machine Code" (http://www.pllab.riec.tohoku.ac.jp/~ohori/research/LogicalMachineRevOct2005.pdf).

      Unfortunately none of the research compilers or languages (including Cyclone) evolved into something 'real'. Maybe Microsoft will release "Verified C#" with Visual Studio 2011??? Smiley

      Thanks for putting these two on, really cool to see!


    • Heavens​Revenge

      Typed ASM should stay a research exercise.... Charles you usually over-hype this typed ASM for maybe for how cool it sounds. I don't think TAL is really a useful or productive mechanism in most ways/shapes/forms for the sum of these parts don't make a greater whole.  And I usually love cutting-edge research projects which try something new, but verification should stay up in a higher level.

      It would make more sense of have Intel and AMD make type-system's with API's and CPU flags which can allow the CPU itself to "type-check" the machine code jammed down it's pipeline. But for ASM source code to have that sort of overhead in the general case is complete overkill...  I think It's easier to have comments left in the ASM source and just as good to have signed and checksummed binaries which are verified by vendors and enthusiasts like me. Malicious coders will fake type safety just as easily if required since security can always be broken, I'd argue that it's even more fragile down there since there's less layers and encapsulation to prevent incorrect code from trying to run when it does happen.

      The ONLY way that a typed ASM may be used I can think of is to reverse engineer binaries into whatever source code language you want as long as it is strongly typed.  Instead of just reverse engineering the binary into the original source code language for it to have actual meaning.

      Verve would undoubtedly benefit from this sort of work and for projects similar to Verve, but its application is way too small for this type of research to benefit anything but a statically verifiable kernel and theorem provers.

      Continue the good work but I hope Hawblitzel moves on to even more interesting and beneficial research areas instead of focusing on this particular domain too long unless this exact domain is his passion, in this case hell, take my words as a grain of salt, I'll never suggest a true researcher to research anything but what he/she loves. Smiley

    • Charles

      @HeavensRevenge: Fine. Smiley In my defense, however, it's not really over-hyped geek marketing of TAL... Rationally, I disagree with you regarding its usefulness. It's at least as useful as IL... Anyway, we do talk about it's usefulness outside the scope of academia.

      Did you watch this video (or listen to it)?  (Sorry about how loud my voice is - I need to move further behind the camera or just get lav mics and a new camera that supports them... Also, I purposely kept the conversation at a higher level, though not too high, since the more techincal audience can get more details from the related papers linked to in the description).

      TAL is as much about building better/more reliable/verifiable compilers as it is about building machine-verifiable software systems, beginning just above the machine (assembly is the lowest level of human-readable software abstraction) and ending up in the playful, cozy bubbles of user experience... Then, yes, there's the over-Charles-hyped uber coolness factor of downloading typed x86 from some service and executing it without remorse (well...)... Smiley

      Keep on pushing the envelope Chris and Juan. Yours is a bright future.
      C

    • felix9

      Juan Chen on Channel 9 finally! Cool stuff, thank you Charles. Smiley

    • Charles

      @felix9: My hope is that she will reappear.
      C

    • Apz

      This is one of final check of compiler to make sure codes generated correctly. There were few bugs related to c# codes that compiler create a big hole when executed. This is a big safety check

    • new2STL

      Very good video, made ​​me feel excited again Smiley

      The first time I was teaching was Operating Systems, some years ago. Good times. I have heard some stuff about Microsoft research on experimental OS that uses a sort of C#, it's good know now what it is and how it works. My old friend, who teaches Compilers will be interested in this video.

      @Charles: More good people to the friends list to make videos! Thank Hawblitzel and Chen and for us.

    • burgosa

      TAL doesn't make sense to me.
      Both C# and MSIL are type safe so TAL isn't needed.
      So the code is checked 2 times.

      To me TAL is just a waste of time, money and cpu cycles.

      If TAL is usable on C++ (for real programmer) then the compiler team can use this as a internal verification thingy.
      (visual studio compiler do have many bugs, too many!!)

      other then that plain waste.
      Just another vista-idea i say. (Slow, waste of time, hardware hungry, etc ,etc... )

    • AnotherKIKI

      Another layer of indirection to slow things...

    Comments closed

    Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums, or Contact Us and let us know.