{"id":239102,"date":"2016-06-16T09:22:25","date_gmt":"2016-06-16T16:22:25","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&#038;p=239102"},"modified":"2020-09-04T16:50:04","modified_gmt":"2020-09-04T23:50:04","slug":"checked-c","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/checked-c\/","title":{"rendered":"Checked C"},"content":{"rendered":"<p>The Checked C project is extending the C programming language so that programmers can write more secure and reliable C programs. The project is developing an extension to C called Checked C that adds checking to C to detect or prevent common programming errors such as buffer overruns, out-of-bounds memory accesses, and incorrect type casts. The extension is designed to be used for existing system software written in C.<\/p>\n<div class=\"conM \">\n<h2>Finding out more<\/h2>\n<p>Here is quick list of resources:<\/p>\n<ul>\n<li>Visit the Checked C <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/Microsoft\/checkedc\/wiki\">Wiki<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> on GitHub to learn more about the Checked C extension.<\/li>\n<li>Download a fork of the clang compiler for trying out Checked C on Windows <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/Microsoft\/checkedc-clang\/releases\">here<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/li>\n<li>The latest version of the Checked C language extension design\u00a0is available on GitHub <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"https:\/\/github.com\/Microsoft\/checkedc\/releases\/download\/v0.7-final\/checkedc-v0.7.pdf\" target=\"_blank\" rel=\"noopener noreferrer\">here.<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>We do all of our on-going work on Github, with repos for the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/microsoft\/checkedc\">language design<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> and <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/microsoft\/checkedc-clang\">compiler implementation.<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>Checked C is an open, collaborative project.\u00a0 Developers and researchers are welcome to try it out, provide feedback, or contribute to the efforts.<\/p>\n<p>Researchers working on the project include <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cs.umd.edu\/~mwh\/\">Michael Hicks<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.cs.umd.edu\/people\/rchen\">Ray Chen<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, and <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.linkedin.com\/in\/hasan-touma\/\">Hasan Touma<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> at the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.umd.edu\/\">University of Maryland<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/machiry.github.io\/\">Aravind Machiry<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> at UC Santa Barbara, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/jorgenavas.github.io\/\"> Jorge Navas<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> at SRI, and <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/arieg.bitbucket.io\/\"> Arie Gurfinkel<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> at the University of Waterloo, and Andrew Ruef. They have been working a conversion tool for converting C programs to Checked C, as well as converting existing code and providing feedback on the language design. We have also worked in the past with researchers at Samsung. We are grateful to all of our collaborators and interns for their contributions to the project.<\/p>\n<p><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/dtarditi\/\">David Tarditi<\/a> gave a research talk on Checked C at the University of Washington in October, 2016.\u00a0\u00a0\u00a0 The\u00a0<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.youtube.com\/watch?v=pD2YRMRlXVw\">talk<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> is available on YouTube.<\/p>\n<\/div>\n<h2>Current interns (2020)<\/h2>\n<div class=\"conM \">\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/yhsun.me\">Yahui Sun<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Texas A\\&M): Yahui Sun worked on converting networking in MUSL, a widely-used C runtime, to use Checked C.   He also worked on improving error messages explaining why bounds declarations cannot be proved to be valid.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.linkedin.com\/in\/esmaeil-mohammadian-2956ba3a\/\">Esmaeil Mohammadian Koruyeh<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (University of California &#8211; Riverside): Esmaeil worked on converting string process code in MUSL, a widley-used C runtime, to use Checked C.  He also worked on extending the kinds of conditional tests that result in widening of pointers to null-terminated arrays.<\/li>\n<\/div>\n<h2>Past Interns<\/h2>\n<div class=\"conM \">\n<h3>2019<\/h3>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cs.rochester.edu\/u\/jzhou41\/\">Jie Zhou<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (University of Rochester): Jie is working on how to dynamically detect memory management errors such as use after free.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.seas.upenn.edu\/~pardisp\/\">Pardis Pashakhanloo<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Univ. of Pennsylvania): Pardis is improving the static checking of bounds declarations in the Checked C compiler.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/cs.uwaterloo.ca\/~anietoro\/\">Abel Nieto<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Univ. of Waterloo): Abel is implementing support for generic data structures in in the Checked C compiler.<\/li>\n<\/ul>\n<h3>2018<\/h3>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.linkedin.com\/in\/shen-liu-50b83441\/\">Shen Liu<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Penn State): \u00a0 Shen worked on static checking for Checked C, including inferring widened bounds for null-terminated arrays.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.linkedin.com\/in\/prabhu-karthikeyan-rajasekaran-2a794412\/\">Prabhu Karthikeyan Rajasekaran<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (UC Irvine).: Prabhu added bounds-safe interfaces for generic functions to Checked C and investigated using Checked C in Linux.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/homes.cs.washington.edu\/~aksimpso\/\">Anna Kornfeld Simpson<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (University of Washington): Anna evaluated Checked C on real-world code, modifying several-open source code bases to use Checked C.<\/li>\n<\/ul>\n<h3>2017<\/h3>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/lenary.co.uk\/\">Sam Elliott<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (University of Washington): Sam worked an implementing the dynamic checking for Checked C.\u00a0 He wrote a <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/lenary.co.uk\/publications\/checkedc_tr02\/\">technical report<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> describing his work in detail.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/www.cs.rutgers.edu\/graduate-students\/jay-lim\">Jay Lim<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Rutgers University): Jay extended the Checked C implementation of clang to support polymorphically-typed functions.\u00a0 This provides a type-safe replacement for many uses of void pointers in C<\/li>\n<\/ul>\n<h3>2016<\/h3>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cs.umd.edu\/~awruef\/\">Andrew Ruef<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (University of Maryland): Andrew wrote a tool for rewriting C programs to use Checked C extensions, specifically the <strong>ptr<\/strong> type.<\/li>\n<\/ul>\n<h2>Detailed Description<\/h2>\n<p>Most system software is written in C or C++, which is based on C. System software includes operating systems, browsers, databases, and programming language interpreters. System software is the \u201cinfrastructure\u201d software that the world runs on.<\/p>\n<p>There are certain kinds of programming errors such as buffer overruns and incorrect type casts that programmers can make when writing C or C++ programs. These errors can lead to security vulnerabilities or software reliability problems. The Checked C extension will let programmers add checking to their programs to detect these kinds of errors when a program runs or while it is being written. Existing system software can be modified incrementally in a backwards-compatible fashion to have this checking.<\/p>\n<p>In C, programmers use pointers to access data. A pointer is the address of a memory cell. It is easy for programmers to make mistakes when working with pointers, such that a program reads or writes the wrong data. These mistakes can cause programs to crash, misbehave, or allow the program to be taken over by a malicious adversary. Checked C allows programmers to better describe how they intend to use pointers and the range of memory occupied by data that a pointer points to. This information is then used to add checking at runtime to detect mistakes where the wrong data is accessed, instead of the error occurring silently and without detection. This information also can be used detect programming errors while the program is being written. The checking is called \u201cbounds-checking\u201d because it checks that data is being accessed within its intended bounds. The name Checked C reflects the fact that static and dynamic checking is being added to C.<\/p>\n<p>Many programming languages already have bounds checking. C# and Java are examples of such languages. However, those languages automatically add the information needed for bounds checking to data structures. This is a problem for system software, where the programmer needs precise control over what a program is doing. In Checked C, the programmer controls the placement of information needed for bounds-checking and how the information flows through the program, so the programmer retains precise control over what a program is doing.<\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>The Checked C project is extending the C programming language so that programmers can write more secure and reliable C programs. The project is developing an extension to C called Checked C that adds checking to C to detect or prevent common programming errors such as buffer overruns, out-of-bounds memory accesses, and incorrect type casts. [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-239102","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2015-05-15","related-publications":[505037],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Chris Hawblitzel","user_id":31425,"people_section":"Group 1","alias":"chrishaw"},{"type":"user_nicename","display_name":"Galen Hunt","user_id":31846,"people_section":"Group 1","alias":"galenh"},{"type":"user_nicename","display_name":"Reuben Olinsky","user_id":33382,"people_section":"Group 1","alias":"reubeno"},{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Group 1","alias":"shuvendu"},{"type":"user_nicename","display_name":"Weidong Cui","user_id":34789,"people_section":"Group 1","alias":"wdcui"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/239102","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":13,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/239102\/revisions"}],"predecessor-version":[{"id":689526,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/239102\/revisions\/689526"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=239102"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=239102"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=239102"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=239102"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=239102"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}