How to express modalities in lambda calculus - are some extensions required?
Are extensions required? Not really. You can take an axiomatic description of a modal logic and simply provide a "primitive" lambda term for each. The modal operators would become type constructors. Haskell's IO monad can be viewed this way. Coherence conditions like the monad laws would provide some conversions between terms.

A different approach, which does involve extending the lambda calculus, is described in Frank Pfenning's and Rowan Davies' A Judgmental Reconstruction of Modal Logic.  Note, this is for an intuitionistic modal logic. This involves changing the context, or specifically, having multiple contexts to include hypothetically valid propositions. You get rules like:$$
\frac{\Delta;\cdot\vdash M : A}{\Delta;\Gamma\vdash\mathsf{box}\ M:\square A}\qquad\frac{\Delta;\Gamma\vdash M:\square A\quad\Delta,u::A;\Gamma\vdash N:B}{\Delta;\Gamma\vdash\mathsf{let\ box}\ u=M\ \mathsf{in}\ N : B}$$
You should read the $\mathsf{let\ box}\ u = M\ \mathsf{in}\dots$ as pattern matching/a destructuring bind against $M$.

We have:$$
(\lambda m.\mathsf{let\ box}\ u= m\ \mathsf{in}\ u) : \square A \to A \\
(\lambda f.\lambda x.\mathsf{let\ box}\ f'=f\ \mathsf{in\ let\ box}\ x'=x\ \mathsf{in\ box}\ (f'x')) : \square(A\to B)\to\square A\to\square B \\
(\lambda m.\mathsf{let\ box}\ u=m\ \mathsf{in\ box}\ (\mathsf{box}\ u)) : \square A \to \square \square A$$
Handling possibility as opposed to or in addition to necessity requires a bit more cleverness.