{"page":"\u003clink rel=\"stylesheet\" href=\"https://lessonplanet.com/assets/packs/css/resources-572d6a42.css\" /\u003e\n\u003clink rel=\"stylesheet\" href=\"https://lessonplanet.com/assets/packs/css/lp_boclips_stylesheets-f4d0de30.css\" media=\"all\" /\u003e\n\u003cdiv data-title='How coders are creating software that\u0026#39;s impossible to hack | Kathleen Fisher' data-url='/boclips/videos/5cf955f749516d367a8e60ee' data-video-url='/boclips/videos/5cf955f749516d367a8e60ee' id='bo_player_modal'\u003e\n\u003cdiv class='boclips-resource-page modal-dialog panel-container'\u003e\n\u003cdiv class='react-notifications-root'\u003e\u003c/div\u003e\n\u003cdiv class='rp-header'\u003e\n\u003cdiv class='rp-type'\u003e\n\u003ci aria-hidden='true' class='fai fa-regular fa-circle-play'\u003e\u003c/i\u003e\nVideo\n\u003c/div\u003e\n\u003ch1 class='rp-title' id='video-title'\u003e\nHow coders are creating software that\u0026#39;s impossible to hack | Kathleen Fisher\n\u003c/h1\u003e\n\u003cdiv class='rp-actions'\u003e\n\u003cdiv class='mr-1'\u003e\n\u003ca class=\"btn btn-success\" data-posthog-event=\"Signup: LP Signup Activity\" data-posthog-location=\"body_link_boclips\" data-remote=\"true\" href=\"/subscription/new\"\u003e\u003cspan\u003e\u003cspan\u003eGet Free Access\u003c/span\u003e\u003cspan class=\"\"\u003e for 10 Days\u003c/span\u003e\u003cspan\u003e!\u003c/span\u003e\u003c/span\u003e\u003c/a\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003cdiv class='rp-body'\u003e\n\u003cdiv class='rp-info'\u003e\n\u003cdiv aria-label='Hide resource details' class='rp-hide-info' role='button' tabindex='0'\u003e\u0026times;\u003c/div\u003e\n\u003ci aria-label='Expand resource details' class='rp-expand-info fai fa-solid fa-up-right-and-down-left-from-center' role='button' tabindex='0'\u003e\u003c/i\u003e\n\u003ci aria-label='Compress resource details' class='rp-compress-info fai fa-solid fa-down-left-and-up-right-to-center' role='button' tabindex='0'\u003e\u003c/i\u003e\n\u003cdiv class='rp-rating'\u003e\n\u003cspan class='resource-pool'\u003e\n\u003cspan class='pool-label'\u003ePublisher:\u003c/span\u003e\n\u003cspan class='pool-name'\u003e\n\u003cspan class='text'\u003e\u003ca data-publisher-id=\"30355360\" href=\"/search?publisher_ids%5B%5D=30355360\"\u003eBig Think\u003c/a\u003e\u003c/span\u003e\n\u003c/span\u003e\n\u003c/span\u003e\n\u003c/div\u003e\n\u003cdiv class='rp-description'\u003e\n\u003cspan class='short-description'\u003eHackers thrive on human error, but a new method of coding is ending that. Recent developments by the HACMS (High-Assurance Cyber Military Systems) program at DARPA has allowed computer scientists to use mathematical proofs to verify that...\u003c/span\u003e\n\u003cspan class='full-description hide'\u003eHackers thrive on human error, but a new method of coding is ending that. Recent developments by the HACMS (High-Assurance Cyber Military Systems) program at DARPA has allowed computer scientists to use mathematical proofs to verify that code—up to 100,000 lines of it at a time—is functionally correct and free of bugs. Kathleen Fisher, professor of computer science and former program manager at DARPA, explains how this allows coders to build a thin base of hyper-secure code that is verified to be functionally correct, \"and then you can have lots of software running on top of it that doesn’t have that same level of assurance associated with it but that you can prove: it doesn’t matter what it does, it’s not going to affect the operation of the overall system.\" To illustrate this technology in the real world, Fisher tells the story of how this new method of coding defended a Boeing Little Bird helicopter from a \"red team\" of hackers charged with causing havoc in the system and bringing that baby down. So is there anything hackers can't hack? Now there is, thanks to the beauty (and rigor) of formal mathematics. Read more at BigThink.\u003ca href='http://bigthink.com/videos/kathleen-fisher-how-coders-are-creating-software-thats-impossible-to-hack' target='_blank' rel='nofollow'\u003ecom\u003c/a\u003e Follow Big Think here: \u003ca href='http://goo.gl/CPTsV5' target='_blank' rel='nofollow'\u003eYouTube\u003c/a\u003e \u003ca href='https://www.facebook.com/BigThinkdotcom' target='_blank' rel='nofollow'\u003eFacebook\u003c/a\u003e \u003ca href='https://twitter.com/bigthink' target='_blank' rel='nofollow'\u003eTwitter\u003c/a\u003e Transcript: HACMS is a program at DARPA that ran for four-and-a-half years that was focused on using techniques from what is called the 'formal methods community', so techniques based on math more or less, to produce software for vehicles that came with proofs that the software had certain desirable properties; that parts of it were functionally correct, that there were no certain kinds of bugs in the software. And the consequence of those proofs is that the system is much harder to hack into. So the formal methods community has been promising for, like, 50 years that they could produce software that proveably didn’t have certain kind of vulnerabilities. And for more or less 50 years they have failed to deliver on that promise. Yes, they could produce proofs of correctness for code but for ten lines of code or 100 lines of code—not enough code to make a difference for any kind of practical purpose. But recently there have been advances in a bunch of different research areas that have changed that equation, and so now formal methods researchers can prove important properties about code bases that are 10,000 or 100,000 lines of code. And that’s still small potatoes compared to the size of Microsoft Windows or the size of Linux which are millions, hundreds of millions of lines of code. But when you start to get to 10,000 or 100,000 lines of code there are really interesting software artifacts that fit in that size. Things like compilers and microkernels, and you can leverage those kinds of exquisite artifacts to build much more complex software systems where only a small part of the system has to be verified to be functionally correct, and then you can have lots of software running on top of it that doesn’t have that same level of assurance associated with it but that you can prove: it doesn’t matter what it does, it’s not going to affect the operation of the overall system. So, for example, HACMS researchers used the high-assurance code and put it on a Boeing Unmanned Little Bird which is a helicopter that can fly completely autonomously or it can fly with two pilots. And this helicopter has two computers on it: one is the mission control computer that controls things like 'fly over there and take a picture' or 'fly over there and take a picture', and communicate to the ground station or the operator who’s telling the helicopter what to do. It also has a flight control computer that controls things like altitude hold and stability, sort of the mechanics of flying the helicopter at any given time period. So the researchers put seL4 microkernel, which is a verified microkernel guaranteed to be functionally correct, on the mission control computer, and they used it to create different software partitions. So one of those partitions was responsible for communicating with the ground station. Another one of those partitions was responsible for operating the camera that the helicopter had. The researchers verified that the code in the 'communicate with the ground station' was functionally correct and isolated from the software in the 'control the camera' part. So the camera part was all the legacy software that had previously been on the helicopter to control camera operation.\u003c/span\u003e\n\u003c/div\u003e\n\u003cdiv class='action-container flex justify-between'\u003e\n\u003cbutton aria-expanded='false' aria-label='Read more description' class='rp-full-description' type='button'\u003e\n\u003ci class='fai fa-solid fa-align-left'\u003e\u003c/i\u003e\n\u003cspan id='read_more'\u003eRead More\u003c/span\u003e\n\u003c/button\u003e\n\u003cdiv class='rp-report'\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003cdiv aria-labelledby='resource-details-heading' class='rp-info-section'\u003e\n\u003ch2 class='title' id='resource-details-heading'\u003eResource Details\u003c/h2\u003e\n\u003cdiv class='rp-resource-details clearfix'\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eCurator Rating\u003c/dt\u003e\n\u003cdd\u003e\u003cspan class=\"star-rating\" aria-label=\"4.0 out of 5 stars\" role=\"img\"\u003e\u003ci class=\"fa-solid fa-star text-action\" aria-hidden=\"true\"\u003e\u003c/i\u003e\u003ci class=\"fa-solid fa-star text-action\" aria-hidden=\"true\"\u003e\u003c/i\u003e\u003ci class=\"fa-solid fa-star text-action\" aria-hidden=\"true\"\u003e\u003c/i\u003e\u003ci class=\"fa-solid fa-star text-action\" aria-hidden=\"true\"\u003e\u003c/i\u003e\u003ci class=\"fa-regular fa-star text-action\" aria-hidden=\"true\"\u003e\u003c/i\u003e\u003c/span\u003e\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt class=\"educator-rating-title\"\u003eEducator Rating\u003c/dt\u003e\u003cdd\u003e\u003cdiv class=\"educator-rating-details\" data-path=\"/educator_ratings/rrp_data?resourceable_id=76978\u0026amp;resourceable_type=Boclips%3A%3AVideoMetadata\"\u003e\u003cspan class=\"not-yet-rated\"\u003eNot yet Rated\u003c/span\u003e\u003c/div\u003e\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eGrade\u003c/dt\u003e\u003cdd title=\"Grade\"\u003e6th - 11th\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eSubjects\u003c/dt\u003e\u003cdd\u003e\u003cspan\u003e\u003ca href=\"/search?keywords=cell+structure+and+function\u0026amp;search_tab_id=1\u0026amp;subject_ids%5B%5D=1216220\u0026amp;type_ids%5B%5D=357920\"\u003eAll Subjects\u003c/a\u003e\u003c/span\u003e\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eMedia Type\u003c/dt\u003e\u003cdd\u003e\u003cspan\u003e\u003ca href=\"/search?keywords=cell+structure+and+function\u0026amp;search_tab_id=2\u0026amp;type_ids%5B%5D=357920\u0026amp;type_ids%5B%5D=4543647\"\u003eInstructional Videos\u003c/a\u003e\u003c/span\u003e\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eSource:\u003c/dt\u003e\n\u003cdd\u003e\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eDate\u003c/dt\u003e\n\u003cdd\u003e2019\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003ci aria-hidden='true' class='fai fa-solid fa-language'\u003e\u003c/i\u003e\n\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\u003cdt\u003eAudiences\u003c/dt\u003e\u003cdd\u003e\u003cspan\u003e\u003ca href=\"/search?audience_ids%5B%5D=371079\u0026amp;keywords=cell+structure+and+function\u0026amp;search_tab_id=1\u0026amp;type_ids%5B%5D=357920\"\u003eFor Teacher Use\u003c/a\u003e\u003c/span\u003e\u003c/dd\u003e\u003cdd class=\"text-muted\"\u003e\u003ci class=\"fa-solid fa-lock mr5\"\u003e\u003c/i\u003e2 more...\u003c/dd\u003e\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003cdiv class='detail'\u003e\n\u003cdl\u003e\n\n\u003c/dl\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003cdiv aria-labelledby='educator-ratings-heading' class='rp-info-section'\u003e\n\u003ch2 class='title sr-only' id='educator-ratings-heading'\u003eEducator Ratings\u003c/h2\u003e\n\u003cdiv id=\"educator-ratings-root\"\u003e\u003c/div\u003e\u003cdiv id=\"all-educator-ratings-root\"\u003e\u003c/div\u003e\u003cdiv id=\"educator-rating-form-root\"\u003e\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003cdiv class='rp-resource'\u003e\n\u003cdiv aria-label='Show resource details' class='rp-show-info' role='button' tabindex='0'\u003e\n\u003ci class='fai fa-solid fa-align-left'\u003e\u003c/i\u003e\nShow resource details\n\u003c/div\u003e\n\u003cdiv aria-label='Video player' class='player' id='player-wrapper' role='region'\u003e\n\u003cdiv class='relative container mx-auto' id='lp-boclips-visitor-thumbnail'\u003e\n\u003ca class=\"block\" data-html=\"true\" data-placement=\"bottom\" data-trigger=\"click\" data-content=\"\u003cdiv class=\u0026quot;text-center py-2\u0026quot;\u003e\u003ca class=\u0026quot;bold\u0026quot; href=\u0026quot;/auth/users/sign_in\u0026quot;\u003eSign in\u003c/a\u003e or \u003ca class=\u0026quot;bold text-danger\u0026quot; data-posthog-event=\u0026quot;Signup: LP Signup Activity\u0026quot; data-posthog-location=\u0026quot;body_link_boclips\u0026quot; data-remote=\u0026quot;true\u0026quot; href=\u0026quot;/subscription/new\u0026quot;\u003eJoin Now\u003c/a\u003e\u003c/div\u003e\" data-title=\"Get Full Access\" data-container=\"body\" rel=\"popover\" tabindex=\"0\" aria-label=\"Play video: How coders are creating software that\u0026#39;s impossible to hack | Kathleen Fisher\" href=\"/subscription/new\"\u003e\u003cimg class=\"resource-img img-thumbnail img-responsive z-10 lp-boclips-thumbnail w-full h-full lozad\" alt=\"How coders are creating software that\u0026#39;s impossible to hack | Kathleen Fisher\" title=\"How coders are creating software that\u0026#39;s impossible to hack | Kathleen Fisher\" onError=\"handleImageNotLoadedError(this)\" data-default-image=\"https://static.lp.lexp.cloud/images/attachment_defaults/resource/large/missing.png\" data-src=\"https://static.lp.lexp.cloud/images/attachment_defaults/resource/large/missing.png\" width=\"315\" height=\"220\" src=\"data:image/png;base64,R0lGODlhAQABAAD/ACwAAAAAAQABAAACADs\" /\u003e\n\u003cspan aria-hidden='true' class='flex justify-center items-center bg-white rounded-full w-16 h-16 absolute top-1/2 left-1/2 -mt-8 -ml-8 cursor-pointer z-0 border-2 border-primary drop-shadow-md lp-boclips-thumbnail-playBtn'\u003e\n\u003ci class='fa-solid fa-play text-primary text-3xl ml-1 drop-shadow-xl'\u003e\u003c/i\u003e\n\u003c/span\u003e\n\u003c/a\u003e\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n\u003c/div\u003e\n"}