0

Scaling symbolic evaluation for automated verification of systems code with Serval

Scaling symbolic evaluation for automated verification of systems code with Serval Nelson et al., SOSP’19

Serval is a framework for developing automated verifiers of systems software. It makes an interesting juxtaposition to the approach Google took with Snap that we looked at last time out. I’m sure that Google engineers do indeed take extreme care when building the low level networking code that powers Google’s datacenters, but their fundamental design point was to enable frequent releases for fast iteration, feedback on their designs, and yes, early detection of problems.

Formal verification is at the other end of the spectrum. In theory it enables you to eliminate whole classes of problems and vulnerabilities entirely (in practice perfection is still hard to come by), and so it can be especially valuable in security sensitive situations. But it comes with a very high price tag:

Writing proofs requires a time investment that is usually measured in person-years, and the size of the proofs can be several times or even more that an order of magnitude larger than that of implementation code.

That’s both very expensive and an incredibly long wait for feedback. To invest in formally modelling something, you really Continue reading

0

Why your providers should support IPv6

As enterprises rely more on cloud, colocation and hosting providers, they should check whether their services support IPv6, which can provide better experiences for their customers, partners, suppliers, vendors and employees.Here is a look at how three top infrastructure-as-a-service (IaaS) providers – Amazon Web Services, Microsoft Azure and Google Cloud Platform - stack up for IPv6. There are other IPv6-capable public cloud service providers, but we mention these three to show that there is a broad spectrum of IPv6 capabilities even among the behemoth public clouds.To read this article in full, please click here

0

Using Kustomize with Cluster API Manifests

A topic that’s been in the back of my mind since writing the Cluster API introduction post is how someone could use kustomize to modify the Cluster API manifests. Fortunately, this is reasonably straightforward. It doesn’t require any “hacks” like those needed to use kustomize with kubeadm configuration files, but similar to modifying kubeadm configuration files you’ll generally need to use the patching functionality of kustomize when working with Cluster API manifests. In this post, I’d like to take a fairly detailed look at how someone might go about using kustomize with Cluster API.

By the way, readers who are unfamiliar with kustomize should probably read this introductory post first, and then read the post on using kustomize with kubeadm configuration files. I suggest reading the latter post because it provides an overview of how to use kustomize to patch a specific portion of a manifest, and you’ll use that functionality again when modifying Cluster API manifests.

A Fictional Use Case

For this post, I’m going to build out a fictional use case/scenario for the use of kustomize and Cluster API. Here are the key points to this fictional use case:

1. Three different clusters on AWS are needed. The Continue reading

0

Scavolini Realizes the Value of Architectural Simplicity Across Data Centers

Growth in the new era of digital business is built on three pillars: providing the best customer experience, supporting continuous...

0

Heavy Networking 485: Understanding Edge Exchanges

Guest Alex Marcham returns to Heavy Networking to explore edge exchanges. Like Internet exchanges, the goal of an edge exchange is to provide direct interconnection and traffic exchange between provider networks, but edge exchanges move that infrastructure closer to end users. Alex walks us through how these exchanges work.

The post Heavy Networking 485: Understanding Edge Exchanges appeared first on Packet Pushers.

0

Michael Dell: The Future of Tech Is Autonomous

Dell Technologies announced an on-demand buying model for its products and autonomous...

Read More »

0

Oil And Gas Giants Build Up Their Strategic GPU Reserves

When you are always looking for what platform architecture will be mainstream, you have to look at what those on the bleeding edge are doing to see what the leading edge might do, which in turn tells you what everyone else might eventually do. …

Oil And Gas Giants Build Up Their Strategic GPU Reserves was written by Timothy Prickett Morgan at The Next Platform.

0

Tech Bytes: Enabling Agility And Security With Tufin Policy Automation (Sponsored)

On today's Tech Bytes, our sponsor is Tufin, and we’re going to dig into the concept of agility in the enterprise, particularly as organizations adopt cloud services and container-based applications. Our guest is Aleck Brailsford, Director of Sales Engineering for the Americas at Tufin.

0

Tech Bytes: Enabling Agility And Security With Tufin Policy Automation (Sponsored)

On today's Tech Bytes, our sponsor is Tufin, and we’re going to dig into the concept of agility in the enterprise, particularly as organizations adopt cloud services and container-based applications. Our guest is Aleck Brailsford, Director of Sales Engineering for the Americas at Tufin.

The post Tech Bytes: Enabling Agility And Security With Tufin Policy Automation (Sponsored) appeared first on Packet Pushers.

0

The HPC Community Should Lead In Composability

It is a rare HPC cluster that is actually upgraded – meaning some of the components in the servers or the networks or the storage that comprise the system are swapped out somewhere about halfway through its lifecycle and replaced with cheaper, faster, or more capacious components. …

The HPC Community Should Lead In Composability was written by Timothy Prickett Morgan at The Next Platform.

0

TM Forum Claims Open API Adoption Up Amid Vendor Lag

More than 50 communications service providers and technology companies have signed on to TM Forum's...

Read More »

0

Telefónica Commits to TIP’s Open Mobile Transport Tech

The carrier says it will be commercially deploying the open mobile transport protocol at scale in...

Read More »

0

USPS invests in GPU-driven servers to speed package processing

The U.S. Postal Service is set to purchase GPU-accelerated servers from Hewlett Packard Enterprise that it expects will help accelerate package data processing up to 10 times over previous methods.The plan is for a spring 2020 deployment, using HPE's Apollo 6500 servers, which come with up to eight Nvidia V100 Tensor Core GPUs. The Postal Service also will use Nvidia's EGX edge computing servers at nearly 200 of its processing locations in the U.S. READ MORE: How AI can improve network capacity planningTo read this article in full, please click here

0

Sponsored Post: Fauna, Sisu, Educative, PA File Sight, Etleap, PerfOps, Triplebyte, Stream

Who's Hiring? 

• Sisu Data is looking for machine learning engineers who are eager to deliver their features end-to-end, from Jupyter notebook to production, and provide actionable insights to businesses based on their first-party, streaming, and structured relational data. Apply here.


• Triplebyte lets exceptional software engineers skip screening steps at hundreds of top tech companies like Apple, Dropbox, Mixpanel, and Instacart. Make your job search O(1), not O(n). Apply here.


• Need excellent people? Advertise your job here! 

Cool Products and Services

• Stateful JavaScript Apps. Effortlessly add state to your Javascript apps with FaunaDB. Generous free tier. Try now!


• Grokking the System Design Interview is a popular course on Educative.io (taken by 20,000+ people) that's widely considered the best System Design interview resource on the Internet. It goes deep into real-world examples, offering detailed explanations and useful pointers on how to improve your approach. There's also a no questions asked 30-day return policy. Try a free preview today.


• PA File Sight - Actively protect servers from ransomware, audit file access to see who is deleting files, reading files or moving files, and detect file copy activity from the server. Historical audit reports Continue reading

0

Money Moves: October 2019

Digital Reality dropped billions on European expansion; Ciena closed its acquisition of Centina;...

Read More »

0

Tooling Up For Exascale

The importance of achieving exascale computing has been discussed at great length in this publication and elsewhere. …

Tooling Up For Exascale was written by Michael Feldman at The Next Platform.

0

Beyond Thin Branch: Move Network Functions to Cloud

In-net SD-WAN allows maximum service delivery with minimum customer premises equipment (CPE)...

Read More »

0

Nyansa Ties Cisco, HPE, Juniper Support Into Voyance Platform

The software lets customers consolidate their network monitoring and telemetry into a single...

Read More »

0

BrandPost: Migrating to SD-WAN? Avoid these Pitfalls, Say IT Leaders

Whether you’re switching from MPLS or Internet VPNs, SD-WAN can jumpstart network performance, agility, and scalability, particularly for cloud applications. However, as with any migration, there can be challenges and surprises. Don’t squash productivity with unplanned outages or security breaches. Plan your migration carefully, ask the right questions, and cover your bases. Here are some key pitfalls to avoid from those who’ve been there.Security Should Work with Your SD-WAN If you’re used to backhauling cloud traffic through data-center security via MPLS, you’re bound to see a big boost in branch office cloud performance using direct Internet access. However, bypassing data-center security means you must find a way to deliver the same level of security at the branch-office level or risk a data breach. Last year, enterprises with completed SD-WAN deployments were 1.3 times more likely to experience a branch-office security breach than without, Shamus McGillicudy, Research Director at analyst firm Enterprise Management Associates reported on a recent webinar.To read this article in full, please click here

0

Network Break 260: Pica8 Launches Campus Automation Framework; VMware Adds IPS To NSX

Brad Casemore from IDC joins Network Break as a guest commentator, and we've got a ton to talk about, including a new campus automation framework from Pica8, new IPS capabilities in VMware's NSX, the release of a limited beta for VMware's Kubernetes wrangler Tanzu Mission Control, an Infoblox acquisition, and more FU than you can shake a virtual donut at.