학술논문

Formally Verifying Function Scheduling Properties in Serverless Applications
Document Type
Periodical
Source
IT Professional IT Prof. IT Professional. 25(6):94-99 Jan, 2023
Subject
Computing and Processing
Engineering Profession
Components, Circuits, Devices and Systems
Power, Energy and Industry Applications
Codes
Databases
Scalability
Regulation
Security
Resource management
Cloud computing
Serverless computing
Costs
Formal verification
Language
ISSN
1520-9202
1941-045X
Abstract
Function as a service (FaaS) is a serverless cloud execution model offering cost-efficiency, scalability, and simplified development by enabling developers to focus on code and delegate server management and application scaling to the serverless platform. Early FaaS implementations provided no control to users over function placement, but raising data locality-bound scenarios motivated new implementations with user-defined constraints over function allocations, e.g., to keep functions accessing a database close to the latter, with the aim of reducing latency, enhancing security, or complying with regulations. In this article, we show how, by leveraging the Allocation Priority Policies language—used for controlling function scheduling—and state-of-the-art planning tools, it is possible to enforce security properties and data-locality constraints, thereby guiding the definition of fine-grained serverless scheduling policies.