Information Technology Innovation Resurgence, Confluence, and Continuing Impact (2020) / Chapter Skim
Currently Skimming:
3 Reflections on Resurgence
3 Reflections on Resurgence
Pages 26-46
The Chapter Skim interface presents what we've algorithmically identified as the most significant single chunk of text within every page in the chapter.
Select key terms on the right to highlight them within pages of the chapter.
From page 26... ...
. It is an important mechanism for capturing, combining, and refining research results and making them available in usable form and at low cost to companies and other orga nizations.
|
From page 27... ...
And there is an important lesson from these examples: It is imperative to sustain research funding for important problems through discouraging periods so that new ideas can emerge and so that researchers can pull in new developments, often coming from other areas of IT or even from other fields, that reignite progress. This section presents a few examples of recent resurgent research tracks in IT.
|
From page 28... ...
Virtualization was repurposed by 1990s academic research to allow a single system to run multiple software environments, so that large data centers could flexibly allocate load among servers -- the foundation for cloud computing. • Virtual reality (VR)
|
From page 29... ...
To solve another, delivering video-streaming content to millions of viewers, network protocols and routers were optimized. And when cyberattacks on data centers started exploiting vulnerabilities in software, static analysis techniques developed by formal systems research were adapted and extended to find many of the bugs.
|
From page 30... ...
Creasy, 1966, A Virtual Machine System for the 360/40, Cambridge Scientific Center Report 320-2007, IBM Corporation, Cambridge, MA.
|
From page 31... ...
Virtualization enables cloud computing -- a cloud data center hosts thousands of independent VMs on a smaller number of real machines, each with a rich software stack tailored to its needs. Today's cloud computing environments have replaced many locally run corporate computing environments.
|
From page 32... ...
Second, the cloud provider reaps and passes on many economies of scale in areas such as buying computers; purchasing electric power; building, outfitting, and operating data centers; testing and installing soft ware; offering hot switchover to backup data centers; backing up data; and defend ing against cyberattacks. Third, virtualization changes personnel needs.
|
From page 33... ...
virtual worlds on smartphone displays, computer displays, or immersive 3D displays such as headsets.5 • VR presents VEs using immersive displays, replacing your perception of the physical world around you with virtual elements. The most common and prolific examples today are viewing 360-degree video, informal education, and games.
|
From page 34... ...
VE applications are driven by user inputs from devices such as joysticks, gaming controllers, instrumented gloves, and hand-held "pucks" that report position and orientation. Input devices vary widely depending on the application: flight trainers mock up a cockpit full of switches, knobs, and of course, the control stick.
|
From page 35... ...
• CAVEs, rooms with images projected on all walls in which a user moves to examine a scene, for a totally immersive experience. Only head position, not orientation, is needed to generate appropriate images.
|
From page 36... ...
9 Fortune Business Insights, 2020, "Virtual Reality (VR) Market to Reach USD 57.55 Billion by 2027; Emphasis on Advanced Virtual Solutions by Eminent Companies to Support Growth," press release, September 2, https://www.fortunebusinessinsights.com/press-release/virtual-reality-market-9265; Market Watch, "Virtual Reality Market 2019: Global Industry Size, Demand, Growth, Analysis, Share Revenue and Forecast 2026," September 12, https://www.marketwatch.com/press-release/virtual-reality-market 2019-global-industry-size-demand-growth-analysis-share-revenue-and-forecast-2026-2019-09-12.
|
From page 37... ...
. • Devising socially acceptable headsets and input devices.
|
From page 38... ...
A software ecosystem is likely to grow to support these developments with components such as user interface frameworks, 3D model and scene creators, iconography to navigate virtual worlds, etc. As was the case with the user interfaces dominant today for personal computers (dubbed WIMP: win dows, icons, menus, pointer)
|
From page 39... ...
Verification requires a formal specification that captures the intended behavior of the system being examined; a rigorous process, often requiring construction of mathematical proofs, is then used to establish correctness of an implementation. Although specifications are usually shorter and simpler than the hardware circuits and software code that implements them, it is a challenge to get them right and to express them in a formal way that permits verification.
|
From page 40... ...
Model checking, a formal technique often used to verify correctness of communication protocols used on computer buses or net works, helped address these needs. Amazon Web Services uses formal methods to check configurations of cloud computing components -- for example, to ensure that one customer cannot access another customer's data or interfere with their service.
|
From page 41... ...
Solvers are awarded according to ing been organized in the odd years, and the latter the number of benchmarks solved during the second in even years. SAT and SMT Solvers stage, using the cumulated time required to solve those benchmarks to break ties.
|
From page 42... ...
, but usually the specification can appear as annotations embedded in the implementation. Tools process specifi cations and code to prepare equations for one or more SMT solvers; Microsoft's Z3 is one such open-source tool in wide use today.18 Analysis tools inspect software to detect common coding errors, such as "memory leaks" (allocating memory that is never de-allocated)
|
From page 43... ...
, • seL4: a micro-kernel22 designed to support safety-critical applications; the autonomous helicopter mentioned below uses sel4 for its "mission computer." Today, computer chip design routinely uses formal techniques, supported by commercial CAD tools. Many open-source software tools are available, as are commercial tools and services for software verification.
|
From page 44... ...
Industrial laboratories also performed fundamental research: SMT solvers trace back to a pro cedure developed by Greg Nelson and Derek C Oppen at Digital Equipment Corpo ration in 1980.24 Z3, a solver from Microsoft Research, has had wide impact, both as research and as an open-source tool.25 Today, Microsoft, Amazon Web Services, 24 G
|
From page 45... ...
As an example, a number of Amazon Web Services features use these technologies, including Amazon inspector, S3 block public access, IAM Access Analyzer, and Amazon CodeGuru. In addition, well-publicized internal projects such as a proof of the correctness of the key management store and the boot loader use these techniques.27 Microsoft Research pursues major projects in formal systems, including the Z3 SMT solver.
|
From page 46... ...
Moreover, the OpenSSL implementation had not been formally verified to eliminate this or other vulnerabilities. Today, Amazon Web Services offers an open-source implementation, s2n, which is formally verified with the assistance of Galois, a company that offers verification tools and services.1 1 Galois, Inc., "Proving Amazon's s2n correct," https://galois.com/project/amazon-s2n, accessed July 1, 2020.
|
Key Terms
This material may be derived from roughly machine-read images, and so is provided only to facilitate research.
More
information on Chapter Skim is available.