EDN Admin
Well-known member
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. [ http://www.cs.cornell.edu/talc/" target="_blank Source ]
http://channel9.msdn.com/Shows/Going+Deep/Verve-A-Type-Safe-Operating-System" target="_blank Youve met Microsoft research scientist and operating system expert Chris Hawblitzel before . Hes the architect and lead researcher of the http://research.microsoft.com/apps/pubs/?id=122884" target="_blank 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 didnt spend much time on TAL during the Verve interview, so we decided to remedy that. Enter computer scientist and http://research.microsoft.com/en-us/groups/rise/default.aspx" target="_blank RiSE team member http://research.microsoft.com/en-us/people/juanchen/" target="_blank Juan Chen who did much of the TAL work for Verve. Tune in and get a sense of what TAL is, how type verification works for assembly code, benefits, trade-offs, and much more. Enjoy. <img src="http://m.webtrends.com/dcs1wotjh10000w0irc493s0e_6x1g/njs.gif?dcssip=channel9.msdn.com&dcsuri=http://channel9.msdn.com/Feeds/RSS&WT.dl=0&WT.entryid=Entry:RSSView:5edac2dcadcc4b2e93b79ecc016c6f8d
View the full article
http://channel9.msdn.com/Shows/Going+Deep/Verve-A-Type-Safe-Operating-System" target="_blank Youve met Microsoft research scientist and operating system expert Chris Hawblitzel before . Hes the architect and lead researcher of the http://research.microsoft.com/apps/pubs/?id=122884" target="_blank 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 didnt spend much time on TAL during the Verve interview, so we decided to remedy that. Enter computer scientist and http://research.microsoft.com/en-us/groups/rise/default.aspx" target="_blank RiSE team member http://research.microsoft.com/en-us/people/juanchen/" target="_blank Juan Chen who did much of the TAL work for Verve. Tune in and get a sense of what TAL is, how type verification works for assembly code, benefits, trade-offs, and much more. Enjoy. <img src="http://m.webtrends.com/dcs1wotjh10000w0irc493s0e_6x1g/njs.gif?dcssip=channel9.msdn.com&dcsuri=http://channel9.msdn.com/Feeds/RSS&WT.dl=0&WT.entryid=Entry:RSSView:5edac2dcadcc4b2e93b79ecc016c6f8d
View the full article
