Browse Source

Initial blueprint

master
Martins Eglitis 2 months ago
commit
c96e3f6478
4 changed files with 877 additions and 0 deletions
  1. +2
    -0
      .gitignore
  2. +686
    -0
      Martins_Eglitis_Master_Thesis_Proposal.lyx
  3. BIN
      Martins_Eglitis_Master_Thesis_Proposal.pdf
  4. +189
    -0
      library.bib

+ 2
- 0
.gitignore View File

@@ -0,0 +1,2 @@
*~
*#

+ 686
- 0
Martins_Eglitis_Master_Thesis_Proposal.lyx View File

@@ -0,0 +1,686 @@
#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass article
\begin_preamble
\usepackage{inputenc}

\usepackage{natbib}
\usepackage{hyperref}

\usepackage{graphicx}

\usepackage[colorinlistoftodos]{todonotes}

\usepackage{parskip}
\setlength{\parskip}{10pt}

\usepackage{tikz}
\usetikzlibrary{arrows, decorations.markings}

\usepackage{chngcntr}
\counterwithout{figure}{section}
\end_preamble
\use_default_options true
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures true
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 1
\use_minted 0
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 2
\tocdepth 2
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style english
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
begin{titlepage}
\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
centering
\end_layout

\end_inset


\end_layout

\begin_layout Standard

\shape smallcaps
\size largest
Master thesis project proposal
\begin_inset Newline newline
\end_inset


\end_layout

\begin_layout Standard
\begin_inset VSpace 0.5cm
\end_inset


\end_layout

\begin_layout Standard

\series bold
\size huge
Tracing in Distributed Systems
\end_layout

\begin_layout Standard
\begin_inset VSpace 2cm
\end_inset


\end_layout

\begin_layout Standard

\size larger
Martins Eglitis eglitis@student.chalmers.se
\end_layout

\begin_layout Standard
\begin_inset VSpace 1.5cm
\end_inset


\end_layout

\begin_layout Standard

\size large
Relevant completed courses:
\end_layout

\begin_layout Itemize
EDA093, Operating Systems
\end_layout

\begin_layout Itemize
EDA387, Computer Networks
\end_layout

\begin_layout Itemize
DAT105, Computer Architecture
\end_layout

\begin_layout Itemize
EDA263, Computer Security
\end_layout

\begin_layout Itemize
EDA491, Network Security
\end_layout

\begin_layout Standard
\begin_inset VSpace vfill
\end_inset


\end_layout

\begin_layout Standard
\begin_inset VSpace vfill
\end_inset


\end_layout

\begin_layout Standard

\size large
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
today
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
end{titlepage}
\end_layout

\end_inset


\end_layout

\begin_layout Section
Introduction
\end_layout

\begin_layout Standard
Distributed systems are ubiquitious, providing daily services such as network
applications (web search, online shopping, gaming), communications (networks,
sensors), transportation, etc.
Although there is no single definition of a distributed system, it can
be perceived as a single point service in the frontend, which is backed
by multiple computers communicating over network.
\end_layout

\begin_layout Standard
In many situations, the number of actual computers that serve a single goal
is tremendous.
For example, there are thousands of nodes involved in serving a web request
when using the google search engine.
Besides the user-defined goal, other tangential goals such as statistics,
spell checker, advertisment are being executed.
The execution trace often leads outside the boundaries of a single network
or datacenter or team or company.
\end_layout

\begin_layout Standard
The real life situation is that these individual instances have little in
common.
They can be developed by different teams in different countries, using
different programming languages and frameworks.
Yet when an error occurs somewhere in the trace, it is crucial to point
to the problematic service.
The main problem is usually the massive scale of the system and current
state-of-the-art monitoring systems can only observe such unwanted event
happening.
For example, observing increase in latencies is possible but it is hard
to pinpoint the actual root cause of the problem, or at least localize
as much as possible.
Even if the problem has been localized in one service, another problem
arises - how to relate the record in the log file to other log files? How
to do it efficiently accross thousands of nodes? How to make sure that
it is the correct service? How to get a single stack trace for the call,
which may involve multiple machines?
\end_layout

\begin_layout Standard
It is therefore very important for developers, managers, network operators,
etc.
to get as close as possible to the root cause of the problem.
\end_layout

\begin_layout Section
Context
\end_layout

\begin_layout Standard
On of the earlier works in the field of tracing in distributed systems presents
Drapper.
Google has been using the closed-source tracer in their production environments
for at least 2 years, making it a mature solution.
The initial requirements for the tracer were: 1) Low overhead - some applicatio
ns are very sensitive to network data increase or latency.
2) Application level transparency - teams and developers are not keen changing
their codebase on demand therefore the tracing has to be implemented in
lower levels, for example, in common libraries (threading, control-flow,
RPC).
3) Scalability and maintainability - Drapper has to be able to support
existing and new services for at least 5 years.
Drapper has the ability to adapt the sampling rate accoring to preset values.
Drapper is using the annotation based tracing, which means that each span
adds extra information to the trace.
\end_layout

\begin_layout Standard

\end_layout

\begin_layout Section
Goals and challenges
\end_layout

\begin_layout Standard
The main goals for the project are:
\end_layout

\begin_layout Itemize
Research state of the art on distributed tracing.
\end_layout

\begin_layout Itemize
Define the tracing data model.
For example, sampling rates, entry points, system components, integration
with other observability methods.
\end_layout

\begin_layout Itemize
Write low overhead code and encapsulate in libraries or applications.
\end_layout

\begin_layout Itemize
Integrate with a tracing collector such as Zipkin, X-Ray, AppDynamics.
\end_layout

\begin_layout Itemize
Evaluate the code based on relevant metrics.
For example, network data overhead and latency, system resource usage (CPU,
memory, storage), scalability, ease of implementation and transparency.
\end_layout

\begin_layout Standard
Some of the challenges are:
\end_layout

\begin_layout Itemize
Due to the nature of the internship and lack of security clearance, some
parts of the system might not be accessible.
\end_layout

\begin_layout Itemize
Enterprise networking products can have large code base and are usually
written in
\begin_inset Quotes eld
\end_inset

low-level
\begin_inset Quotes erd
\end_inset

languages such as C/C+.
It makes the learning curve steep.
\end_layout

\begin_layout Itemize
Existing products might not be homogenous and implementing code will thus
require more individual adjustments accross the instrumentation libraries.
\end_layout

\begin_layout Itemize
All non-trivial software is known to potentially contain bugs introducing
security vulnerabilities, unwanted program behavior [CITATION 3].
All these factors can impact the speed and quality of development.
\end_layout

\begin_layout Section
Approach
\end_layout

\begin_layout Standard
Initial work will consist of reading related sources to
\end_layout

\begin_layout Section
Notes
\end_layout

\begin_layout Standard
Some forms of the communication include HTTP requests, RPC calls, etc.
Distributed systems are becoming more and more ubiquitious.
\end_layout

\begin_layout Standard
Specialized hardware used to dominate the market and provided network-related
functionality like packet forwarding or firewalls.
During the last decade, more and more users and companies are migrating
to so called network functions (NF), mainly due to increased maintainability
and scalability the software-based approach offers.
However it also has downsides - non-trivial software is known to potentially
contain bugs introducing security vulnerabilities, unwanted program behavior,
etc.
\begin_inset CommandInset citation
LatexCommand cite
key "zaostrovnykhVerifyingSoftwareNetwork2019"
literal "false"

\end_inset


\end_layout

\begin_layout Standard
The language of choice for developers to write NF is usually C.
It comes from the fact that the kernel, referring to the Linux kernel in
this project, utilities and libraries are heavily using the language.
Yet being a developer competent in building NFs does not automatically
mean being interested in verification.
NFs being an integral part of the network naturally
\begin_inset CommandInset citation
LatexCommand cite
key "martinsClickOSArtNetwork"
literal "false"

\end_inset

requires proof of correctness, however verification should put a negligible
burden to developers.
\end_layout

\begin_layout Standard
There are reasons which make ASIC-based home routers an interesting target
for research and conversion to verifiable NFs: 1) Improved flexibility
- users no longer dependant on vendor updates or hardware.
2) Deployment costs - NFs do not require expensive hardware, virtualization
is possible.
3) Sandboxing - the scope is more local when compared to operator environments,
which is the usual deployment environment
\begin_inset CommandInset citation
LatexCommand cite
key "martinsClickOSArtNetwork"
literal "false"

\end_inset

.
\end_layout

\begin_layout Standard
There are three parts this project will focus on - NFs, verification, and
home routers.
The problem is to identify which NFs makes a simple, yet fully functional
home router, develop the missing NFs and verify the correctness.
This project will build on the results (e.g., a NAT and a firewall NFs) presented
in the earlier papers
\begin_inset CommandInset citation
LatexCommand cite
key "pirelliFormallyVerifiedNAT2018,zaostrovnykhFormallyVerifiedNAT2017,zaostrovnykhVerifyingSoftwareNetwork2019"
literal "false"

\end_inset

.
\end_layout

\begin_layout Section
Context
\end_layout

\begin_layout Standard
A formally verified NAT was introduced in an earlier work
\begin_inset CommandInset citation
LatexCommand cite
key "zaostrovnykhFormallyVerifiedNAT2017"
literal "false"

\end_inset

.
It was then was then extended
\begin_inset CommandInset citation
LatexCommand cite
key "pirelliFormallyVerifiedNAT2018"
literal "false"

\end_inset

by verifying not only the exact NF but also the whole stack, including
kernel bypass framework (DPDK) and a NIC driver (Intel ixgbe).
Recent work presented Vigor, a software toolchain for building and verifying
NFs, which is used to
\begin_inset Quotes eld
\end_inset

verify low-level properties memory safety, crash freedom, hang freedom,
absence of undefined behavior
\begin_inset Quotes erd
\end_inset

.
For a proof-of-concept, five different NLs were presented - a NAT, a Maglev
load balancer, a MAC-learning bridge, a firewall, and a traffic policer.
Based on the input specification Vigor yields success or a counter-example
upon failure
\begin_inset CommandInset citation
LatexCommand cite
key "zaostrovnykhVerifyingSoftwareNetwork2019"
literal "false"

\end_inset

.
\end_layout

\begin_layout Standard
Earlier work on ClickOS, a modular router, introduced a table of 18 modular
elements for building a middlebox, thus giving intuition of possible NFs
for a home router
\begin_inset CommandInset citation
LatexCommand cite
key "martinsClickOSArtNetwork"
literal "false"

\end_inset

.
Gravel, another similar toolchain to Vigor, is used to verify ClickOS's
elements.
Both Gravel and Vigor use extensive symbolic execution, differences occur
when handling code that can not be symbolically executed.
However, Vigor will be used in this project because: 1) It already provides
the majority of components required for building missing NFs.
2) A side objective of the project is to actually combine all Vigor-verifyied
NFs of a home router in a functional software middlebox.
\end_layout

\begin_layout Section
Goals and Challenges
\end_layout

\begin_layout Standard
The main goals for the project are:
\end_layout

\begin_layout Enumerate
Identify essential NFs required for a home router.
\end_layout

\begin_layout Enumerate
Design, build and evaluate the missing NFs.
\end_layout

\begin_layout Enumerate
Write specifications based on RFCs, IEEE standards, etc.
\end_layout

\begin_layout Enumerate
Verify the NFs against given specifications.
\end_layout

\begin_layout Enumerate
Add functionality to the existing Vigor toolchain if required.
\end_layout

\begin_layout Standard
Some of the challenges are:
\end_layout

\begin_layout Enumerate
Finding the set of NFs is highly subjective for each use case.
\end_layout

\begin_layout Enumerate
Writing NFs such as IPS might be challenging.
\end_layout

\begin_layout Enumerate
Toolchain (libVig) lacks some primitives for cypto and regexp
\begin_inset CommandInset citation
LatexCommand cite
key "zaostrovnykhVerifyingSoftwareNetwork2019"
literal "false"

\end_inset

.
\end_layout

\begin_layout Enumerate
NFs are not always documented, e.g.
for monitoring and configuration.
\end_layout

\begin_layout Enumerate
A good understanding of the exact NF and the whole stack is required.
\end_layout

\begin_layout Enumerate
Verification might take infinite time if done incorrectly, e.g.
path explosion.
\end_layout

\begin_layout Enumerate
Previous verification required significant system resources for full stack
(700 GB RAM, 28 cores, 1 hour clock time)
\begin_inset CommandInset citation
LatexCommand cite
key "zaostrovnykhVerifyingSoftwareNetwork2019"
literal "false"

\end_inset

.
\end_layout

\begin_layout Enumerate
Bugs lower in the stack (e.g.
DPDK, ixgbe) might interfere with NFs.
\end_layout

\begin_layout Section
Approach
\end_layout

\begin_layout Standard
Initial work will consist of reading related sources to specify the core
NFs of a home router.
ClickOS as of now holds 21 elements (NFs), which might be used as inspiration.
Elements are written in C++ thus a rewrite to C will be required.
Another aspect that has to be taken into account is documentation which,
if exists, will define the behavior of the NF, regardless of existing implemene
ntations.
Vigor toolchain will be used to build and run each NF - libVig for data
structures such as expiring hashmaps and number range manager, DPDK as
the IO framework, Intel ixgbe as the network driver, and NFOS as the custom
built operating system.
Python will be used for writing specifications.
Aside from some specifics required by Vigor, the toolchain should not interfere
much with the development process.
Each NF will be extensively verified; in case of failure debug information
will be provided by Vigor and the respective code snippet will be updated
accordingly.
Some NFs evaluation terms will be: 1) Performance - what are the results
(e.g.
latency, throughput) for each NF? How does it compare to other NF implementatio
ns? 2) Verification metrics - how long does it take to verify a particular
NF with or without the underlying software stack?
\end_layout

\begin_layout Standard
\begin_inset CommandInset bibtex
LatexCommand bibtex
btprint "btPrintCited"
bibfiles "/home/martins/Projects/cisco-tracing/docs/library"
options "plain"

\end_inset


\end_layout

\end_body
\end_document

BIN
Martins_Eglitis_Master_Thesis_Proposal.pdf View File


+ 189
- 0
library.bib View File

@@ -0,0 +1,189 @@

@article{alvaroOKWHYTRACING,
title = {{{OK}}, {{BUT WHY}}? {{TRACING AND DEBUGGING DISTRIBUTED SYSTEMS}}},
author = {Alvaro, Peter},
pages = {14},
annote = {[object Object]},
file = {/home/martins/Zotero/storage/86F2V4E6/Alvaro - OK, BUT WHY TRACING AND DEBUGGING DISTRIBUTED SYS.pdf},
language = {en}
}

@article{alvaroOKWHYTRACINGa,
title = {{{OK}}, {{BUT WHY}}? {{TRACING AND DEBUGGING DISTRIBUTED SYSTEMS}}},
author = {Alvaro, Peter},
pages = {14},
file = {/home/martins/Zotero/storage/7BFCUNXD/Alvaro - OK, BUT WHY TRACING AND DEBUGGING DISTRIBUTED SYS.pdf},
language = {en}
}

@misc{AWSReInvent,
title = {{{AWS}} Re:{{Invent}} 2018: {{Deep Dive}} into {{AWS X}}-{{Ray}}: {{Monitor Modern Applications}} ({{DEV324}})},
shorttitle = {{{AWS}} Re},
abstract = {Are you spending hours trying to understand how customers are impacted by performance issues and faults in your service-oriented applications? In this session, we show you how customers are using AWS X-Ray to reduce mean time to resolution, get to the root cause faster, and determine customer impact. In addition, one of our X-Ray customers, ConnectWise,\ presents a\ case study and best practices on how it is\ leveraging X-Ray in its\ production environment. We also show you how to use X-Ray with applications built using AWS services, such as Amazon Elastic Container Service for Kubernetes (Amazon EKS), AWS Fargate, Amazon Elastic Container Service (Amazon ECS), and AWS Lambda\ to achieve the above.}
}

@misc{AWSXRayDistributed,
title = {{{AWS X}}-{{Ray}} \textendash{} {{Distributed Tracing System}}},
abstract = {AWS X-Ray helps you debug and analyze your microservices applications with request tracing so you can find the root cause of issues and performance bottlenecks.},
file = {/home/martins/Zotero/storage/4MG36NPM/xray.html},
howpublished = {https://aws.amazon.com/xray/},
journal = {Amazon Web Services, Inc.},
language = {en-US}
}

@article{DPDK,
title = {{{DPDK}}},
journal = {DPDK},
language = {en-US}
}

@misc{FayExtensibleDistributed,
title = {Fay: {{Extensible Distributed Tracing}} from {{Kernels}} to {{Clusters}} - {{Microsoft Research}}},
file = {/home/martins/Zotero/storage/MA2TJNQ6/fay-extensible-distributed-tracing-from-kernels-to-clusters-2.html},
howpublished = {https://www.microsoft.com/en-us/research/publication/fay-extensible-distributed-tracing-from-kernels-to-clusters-2/}
}

@misc{FayExtensibleDistributeda,
title = {Fay: {{Extensible Distributed Tracing}} from {{Kernels}} to {{Clusters}} - {{Microsoft Research}}},
howpublished = {https://www.microsoft.com/en-us/research/publication/fay-extensible-distributed-tracing-from-kernels-to-clusters-2/}
}

@misc{laineWhyYouNeed2019,
title = {Why You Need {{Tracing}} in Your Distributed Systems},
author = {Laine, Christopher},
year = {2019},
month = may,
abstract = {Don't lose the trees for the forest},
file = {/home/martins/Zotero/storage/PDUNIUGY/why-you-need-tracing-in-your-distributed-systems-c738f0fce088.html},
howpublished = {https://medium.com/it-dead-inside/why-you-need-tracing-in-your-distributed-systems-c738f0fce088},
journal = {Medium},
language = {en}
}

@misc{laineWhyYouNeed2019a,
title = {Why You Need {{Tracing}} in Your Distributed Systems},
author = {Laine, Christopher},
year = {2019},
month = may,
abstract = {Don't lose the trees for the forest},
file = {/home/martins/Zotero/storage/4IN8LA3U/why-you-need-tracing-in-your-distributed-systems-c738f0fce088.html},
howpublished = {https://medium.com/it-dead-inside/why-you-need-tracing-in-your-distributed-systems-c738f0fce088},
journal = {Medium},
language = {en}
}

@article{martinsClickOSArtNetwork,
title = {{{ClickOS}} and the {{Art}} of {{Network Function Virtualization}}},
author = {Martins, Joao and Ahmed, Mohamed and Raiciu, Costin and Olteanu, Vladimir and Honda, Michio and Huici, Felipe},
abstract = {Over the years middleboxes have become a fundamental part of today's networks. Despite their usefulness, they come with a number of problems, many of which arise from the fact that they are hardware-based: they are costly, difficult to manage, and their functionality is hard or impossible to change, to name a few.},
language = {English}
}

@misc{nikmd23DistributedTracingAzure,
title = {Distributed {{Tracing}} in {{Azure Application Insights}} - {{Azure Monitor}}},
author = {{nikmd23}},
abstract = {Provides information about Microsoft's support for distributed tracing through our local forwarder and partnership in the OpenCensus project},
file = {/home/martins/Zotero/storage/KIF6LLC6/distributed-tracing.html},
howpublished = {https://docs.microsoft.com/en-us/azure/azure-monitor/app/distributed-tracing},
language = {en-us}
}

@misc{OpenCensus,
title = {{{OpenCensus}}},
file = {/home/martins/Zotero/storage/KMSVEBJM/opencensus.io.html},
howpublished = {https://opencensus.io/}
}

@misc{PaperDapperGoogle,
title = {Paper: {{Dapper}}, {{Google}}'s {{Large}}-{{Scale Distributed Systems Tracing Infrastructure}} - {{High Scalability}} -},
shorttitle = {Paper},
abstract = {Imagine a single search request coursing through Google's massive infrastructure. A single request...},
file = {/home/martins/Zotero/storage/Y786D2VA/paper-dapper-googles-large-scale-distributed-systems-tracing.html},
howpublished = {http://highscalability.com/blog/2010/4/27/paper-dapper-googles-large-scale-distributed-systems-tracing.html},
language = {en}
}

@misc{PaperDapperGooglea,
title = {Paper: {{Dapper}}, {{Google}}'s {{Large}}-{{Scale Distributed Systems Tracing~Infrastructure}} - {{High Scalability}} -},
file = {/home/martins/Zotero/storage/MMW237EU/paper-dapper-googles-large-scale-distributed-systems-tracing.html},
howpublished = {http://highscalability.com/blog/2010/4/27/paper-dapper-googles-large-scale-distributed-systems-tracing.html}
}

@inproceedings{pirelliFormallyVerifiedNAT2018,
title = {A {{Formally Verified NAT Stack}}},
booktitle = {Proceedings of the 2018 {{Afternoon Workshop}} on {{Kernel Bypassing Networks}} - {{KBNets}}'18},
author = {Pirelli, Solal and Zaostrovnykh, Arseniy and Candea, George},
year = {2018},
pages = {8--14},
publisher = {{ACM Press}},
address = {{Budapest, Hungary}},
doi = {10.1145/3229538.3229540},
abstract = {Prior work proved a stateful NAT network function to be semantically correct, crash-free, and memory safe [29]. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardware to be correct. We extend the toolchain to verify the kernel-bypass framework and a NIC driver in the context of the NAT. We uncover bugs in both the framework and the driver. Our code is publicly available [28].},
isbn = {978-1-4503-5909-2},
language = {English}
}

@article{sigelmanDapperLargeScaleDistributed,
title = {Dapper, a {{Large}}-{{Scale Distributed Systems Tracing Infrastructure}}},
author = {Sigelman, Benjamin H and Barroso, Luiz Andre and Burrows, Mike and Stephenson, Pat and Plakal, Manoj and Beaver, Donald and Jaspan, Saul and Shanbhag, Chandan},
pages = {14},
abstract = {Modern Internet services are often implemented as complex, large-scale distributed systems. These applications are constructed from collections of software modules that may be developed by different teams, perhaps in different programming languages, and could span many thousands of machines across multiple physical facilities. Tools that aid in understanding system behavior and reasoning about performance issues are invaluable in such an environment.},
file = {/home/martins/Zotero/storage/9TFTPSP3/Sigelman et al. - Dapper, a Large-Scale Distributed Systems Tracing .pdf},
language = {en}
}

@misc{WhyYouNeed,
title = {Why You Need {{Tracing}} in Your Distributed Systems - {{IT Dead Inside}} - {{Medium}}},
file = {/home/martins/Zotero/storage/S274RJHD/why-you-need-tracing-in-your-distributed-systems-c738f0fce088.html},
howpublished = {https://medium.com/it-dead-inside/why-you-need-tracing-in-your-distributed-systems-c738f0fce088}
}

@misc{WhyYouNeeda,
title = {Why You Need {{Tracing}} in Your Distributed Systems - {{IT Dead Inside}} - {{Medium}}},
howpublished = {https://medium.com/it-dead-inside/why-you-need-tracing-in-your-distributed-systems-c738f0fce088}
}

@misc{WhyYouNeedb,
title = {Why You Need {{Tracing}} in Your Distributed Systems - {{IT Dead Inside}} - {{Medium}}},
file = {/home/martins/Zotero/storage/BH9QB72L/why-you-need-tracing-in-your-distributed-systems-c738f0fce088.html},
howpublished = {https://medium.com/it-dead-inside/why-you-need-tracing-in-your-distributed-systems-c738f0fce088}
}

@misc{WhyYouNeedc,
title = {Why You Need {{Tracing}} in Your Distributed Systems - {{IT Dead Inside}} - {{Medium}}},
file = {/home/martins/Zotero/storage/8J383XUD/why-you-need-tracing-in-your-distributed-systems-c738f0fce088.html},
howpublished = {https://medium.com/it-dead-inside/why-you-need-tracing-in-your-distributed-systems-c738f0fce088}
}

@inproceedings{zaostrovnykhFormallyVerifiedNAT2017,
title = {A {{Formally Verified NAT}}},
booktitle = {Proceedings of the {{Conference}} of the {{ACM Special Interest Group}} on {{Data Communication}} - {{SIGCOMM}} '17},
author = {Zaostrovnykh, Arseniy and Pirelli, Solal and Pedrosa, Luis and Argyraki, Katerina and Candea, George},
year = {2017},
pages = {141--154},
publisher = {{ACM Press}},
address = {{Los Angeles, CA, USA}},
doi = {10.1145/3098822.3098833},
isbn = {978-1-4503-4653-5},
language = {English}
}

@inproceedings{zaostrovnykhVerifyingSoftwareNetwork2019,
title = {Verifying Software Network Functions with No Verification Expertise},
booktitle = {Proceedings of the 27th {{ACM Symposium}} on {{Operating Systems Principles}} - {{SOSP}} '19},
author = {Zaostrovnykh, Arseniy and Pirelli, Solal and Iyer, Rishabh and Rizzo, Matteo and Pedrosa, Luis and Argyraki, Katerina and Candea, George},
year = {2019},
pages = {275--290},
publisher = {{ACM Press}},
address = {{Huntsville, Ontario, Canada}},
doi = {10.1145/3341301.3359647},
abstract = {We present the design and implementation of Vigor, a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Developers write the core of the middlebox\textemdash{}the network function (NF)\textemdash{}in C, on top of a standard packet-processing framework, putting persistent state in data structures from Vigor's library; the Vigor toolchain then automatically verifies that the resulting software stack correctly implements a specification, which is written in Python. Vigor has three key features: network function developers need no verification expertise, and the verification process does not require their assistance (push-button verification); the entire software stack is verified, down to the hardware (full-stack verification); and verification can be done in a payas-you-go manner, i.e., instead of investing upfront a lot of time in writing and verifying a complete specification, one can specify one-off properties in a few lines of Python and verify them without concern for the rest.},
isbn = {978-1-4503-6873-5},
language = {English}
}

@unpublished{zotero-15,
type = {Unpublished}
}



Loading…
Cancel
Save