Refering to global variables inside modules

Using Symbol is one way:

b = 10;
Module[{b},
 b = 5;
 Symbol["b"]
 ]
(* Out: 10 *)

Your example:

proc[a_] := Module[{b}, b = a;
  {Symbol["b"] -> b}]
b /. proc[1]
(* Out: 1 *)

Using Symbol["b"] as illustrated by Anon works because the renaming by Module takes place before evaluation, but this is not robust in the sense that it is not equivalent to the Symbol b; it is only an expression that evaluates to b. Consider what happens if we try to make an assignment to this expression:

ClearAll[proc, b]
proc[a_] := Module[{b = a}, Symbol["b"] = b]
proc[7]

Set::write: Tag Symbol in Symbol[b] is Protected. >>

The simplest answer is: use a different Symbol name so that there is no conflict. This is not merely a tautology. Ultimately any solution will resolve to this, as using a different Symbol name is the method by which Module itself operates. Even the code above works by this method, though not robustly. Observe:

f[a_] := Module[{b = a}, Hold[Symbol["b"] = b]]

f[7]

Hold[Symbol["b"] = b$289]

The explicit appearances of b in the Module have been replaced with b$289, such that when Symbol["b"] evaluates to b there is no conflict.

We can use this same type of renaming to prevent the collision in the first place. (See Enforcing correct variable bindings and avoiding renamings for conflicting variables in nested scoping constructs for an understanding of the automatic renaming I shall use.)

First an illustration:

ClearAll[f, b]
f[a_] := With[{bb = b}, Hold @ Module[{b = a}, Hold[bb = b]]]
f[7]

Hold[Module[{b$ = 7}, Hold[b = b$]]]

I added a second Hold so that we can observe what happens to the Module: all appearances of the localized symbol are replaced with b$. This is separate from the renaming that takes place because of the Module itself. Continuing the evaluation:

Hold[Module[{b$ = 7}, Hold[b = b$]]] // ReleaseHold

Hold[b = b$580]

We can combine this automatic renaming within scoping constructs with an undocumented With syntax that holds substitution values unevaluated to create a robust method:

ClearAll[proc]

proc[a_] :=
  With[{bb := b},
    Module[{b}, b = 2 a; bb = b]
  ]

Now the assignment is made to global symbol b even if a prior assignment exists:

proc[3]; b
proc[7]; b

6

14

The problem is the Module's local symbols overshadows the global symbols while the Module is being evaluated. One can see this by this example

b = 1;
foo[] := Module[{b = 3},
  Print[b];
  Print[Global`b];
  ]

What do you expect foo[] will print? Will it print 3 1 or 3 3 ?

It prints 3 3. The Globalb has been overshadowed by the local b, even though the Global context was added explicitly.

One way is to explicitly give different context to the global b, like this

my`b = 1;
foo[] := Module[{b = 3},
  Print[b];
  Print[my`b];
  ]

Now it prints 3 1

Another way, is to add a context to each local symbol, like this

b = 1;
foo[] := Module[{foo`b = 3},
  Print[foo`b];
  Print[Global`b];  (* or just  b here *)
  ]

Now it prints 3 1 also. But one can argue that the whole point of using a Module is that one does not have to do this.

The button line is: To be safe, do not access (even if for read only) any global variables. The notebook interface tells by the color of the symbols which symbol is local and which is not.